(* Properties with sort-irrelevant equivalence for terms ********************)
lemma teqx_feqx: ∀T1,T2. T1 ≛ T2 →
- â\88\80G,L. â¦\83G,L,T1â¦\84 â\89\9b â¦\83G,L,T2â¦\84.
+ â\88\80G,L. â\9dªG,L,T1â\9d« â\89\9b â\9dªG,L,T2â\9d«.
/2 width=1 by feqx_intro_sn/ qed.
(* Advanced properties ******************************************************)