731 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"

   731 | a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"

   732 

   732 

   733 thm a3[simplified alpha_gen]

   733 print_theorems

   734 

   735 lemma alpha5_inj:

   736   "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"

   737   "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"

   738   "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = (\<exists>pi. ((bv5 l1, t1) \<approx>gen alpha5 rfv_trm5 pi (bv5 l2, t2) \<and>

   739          (bv5 l1, l1) \<approx>gen alphalts rfv_lts pi (bv5 l2, l2) \<and>

   740          (pi \<bullet> (bv5 l1) = bv5 l2)))"

   741   "rLnil \<approx>l rLnil"

   742   "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2 \<and> n1 = n2)"

   743 apply -

   744 apply (simp_all add: alpha5_alphalts.intros)

   745 apply rule

   746 apply (erule alpha5.cases)

   747 apply (simp_all add: alpha5_alphalts.intros)

   748 apply rule

   749 apply (erule alpha5.cases)

   750 apply (simp_all add: alpha5_alphalts.intros)

   751 apply rule

   752 apply (erule alpha5.cases)

   753 apply (simp_all add: alpha5_alphalts.intros)

   754 apply rule

   755 apply (erule alphalts.cases)

   756 apply (simp_all add: alpha5_alphalts.intros)

   757 done

   758 

   759 lemma alpha5_equivps:

   760   shows "equivp alpha5"

   761   and   "equivp alphalts"

   762 sorry

   763 

   764 quotient_type

   765   trm5 = rtrm5 / alpha5

   766 and

   767   lts = rlts / alphalts

   768   by (auto intro: alpha5_equivps)

   769 

   770