(* Properties on lazy equivalence on closures *******************************)
-lemma fpbc_fleq_trans: â\88\80h,g,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] ⦃G, L, T⦄ →
- â¦\83G, L, Tâ¦\84 â\8b\95[0] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] ⦃G2, L2, T2⦄.
+lemma fpbc_fleq_trans: â\88\80h,g,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] ⦃G, L, T⦄ →
+ â¦\83G, L, Tâ¦\84 â\89¡[0] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 *
/3 width=9 by fleq_trans, ex2_3_intro/
qed-.
-lemma fleq_fpbc_trans: â\88\80h,g,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1, L1, T1â¦\84 â\8b\95[0] ⦃G, L, T⦄ →
- â¦\83G, L, Tâ¦\84 â\89»â\8b\95[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89»â\8b\95[h, g] ⦃G2, L2, T2⦄.
+lemma fleq_fpbc_trans: â\88\80h,g,G1,G,G2,L1,L,L2,T1,T,T2. â¦\83G1, L1, T1â¦\84 â\89¡[0] ⦃G, L, T⦄ →
+ â¦\83G, L, Tâ¦\84 â\89»â\89¡[h, g] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89»â\89¡[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 *
#G0 #L0 #T0 #H0 #H02 elim (fleq_fpbu_trans … H1 … H0) -G -L -T
/3 width=9 by fleq_trans, ex2_3_intro/