(* Properties with degree-based equivalence for closures ********************)
(* Basic_2A1: uses: fleq_fpb_trans *)
-lemma feqx_fpb_trans: â\88\80h,F1,F2,K1,K2,T1,T2. â¦\83F1,K1,T1â¦\84 â\89\9b â¦\83F2,K2,T2â¦\84 →
- â\88\80G2,L2,U2. â¦\83F2,K2,T2â¦\84 â\89»[h] â¦\83G2,L2,U2â¦\84 →
- â\88\83â\88\83G1,L1,U1. â¦\83F1,K1,T1â¦\84 â\89»[h] â¦\83G1,L1,U1â¦\84 & â¦\83G1,L1,U1â¦\84 â\89\9b â¦\83G2,L2,U2â¦\84.
+lemma feqx_fpb_trans: â\88\80h,F1,F2,K1,K2,T1,T2. â\9dªF1,K1,T1â\9d« â\89\9b â\9dªF2,K2,T2â\9d« →
+ â\88\80G2,L2,U2. â\9dªF2,K2,T2â\9d« â\89»[h] â\9dªG2,L2,U2â\9d« →
+ â\88\83â\88\83G1,L1,U1. â\9dªF1,K1,T1â\9d« â\89»[h] â\9dªG1,L1,U1â\9d« & â\9dªG1,L1,U1â\9d« â\89\9b â\9dªG2,L2,U2â\9d«.
#h #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2
#K2 #T2 #HK12 #HT12 #G2 #L2 #U2 #H12
elim (teqx_fpb_trans … HT12 … H12) -T2 #K0 #T0 #H #HT0 #HK0
(* Inversion lemmas with degree-based equivalence for closures **************)
(* Basic_2A1: uses: fpb_inv_fleq *)
-lemma fpb_inv_feqx: â\88\80h,G1,G2,L1,L2,T1,T2. â¦\83G1,L1,T1â¦\84 â\89»[h] â¦\83G2,L2,T2â¦\84 →
- â¦\83G1,L1,T1â¦\84 â\89\9b â¦\83G2,L2,T2â¦\84 → ⊥.
+lemma fpb_inv_feqx: â\88\80h,G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â\89»[h] â\9dªG2,L2,T2â\9d« →
+ â\9dªG1,L1,T1â\9d« â\89\9b â\9dªG2,L2,T2â\9d« → ⊥.
#h #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
[ #G2 #L2 #T2 #H12 #H elim (feqx_inv_gen_sn … H) -H
/3 width=11 by reqx_fwd_length, fqu_inv_teqx/