src/CTT/CTT.thy
changeset 23467 d1b97708d5eb
parent 22808 a7daa74e2980
child 26391 6e8aa5a4eb82
equal deleted inserted replaced
23466:886655a150f6 23467:d1b97708d5eb
   395 apply assumption+
   395 apply assumption+
   396 done
   396 done
   397 
   397 
   398 (*Simplify the parameter of a unary type operator.*)
   398 (*Simplify the parameter of a unary type operator.*)
   399 lemma subst_eqtyparg:
   399 lemma subst_eqtyparg:
   400   assumes "a=c : A"
   400   assumes 1: "a=c : A"
   401     and "!!z. z:A ==> B(z) type"
   401     and 2: "!!z. z:A ==> B(z) type"
   402   shows "B(a)=B(c)"
   402   shows "B(a)=B(c)"
   403 apply (rule subst_typeL)
   403 apply (rule subst_typeL)
   404 apply (rule_tac [2] refl_type)
   404 apply (rule_tac [2] refl_type)
   405 apply (rule prems)
   405 apply (rule 1)
   406 apply assumption
   406 apply (erule 2)
   407 done
   407 done
   408 
   408 
   409 (*Simplification rules for Constructive Type Theory*)
   409 (*Simplification rules for Constructive Type Theory*)
   410 lemmas reduction_rls = comp_rls [THEN trans_elem]
   410 lemmas reduction_rls = comp_rls [THEN trans_elem]
   411 
   411