(* Properties with sort-irrelevant equivalence on referred entries **********)
-lemma aaa_teqx_conf_reqx: â\88\80G,L1,T1,A. â¦\83G,L1â¦\84 ⊢ T1 ⁝ A → ∀T2. T1 ≛ T2 →
- â\88\80L2. L1 â\89\9b[T1] L2 â\86\92 â¦\83G,L2â¦\84 ⊢ T2 ⁝ A.
+lemma aaa_teqx_conf_reqx: â\88\80G,L1,T1,A. â\9dªG,L1â\9d« ⊢ T1 ⁝ A → ∀T2. T1 ≛ T2 →
+ â\88\80L2. L1 â\89\9b[T1] L2 â\86\92 â\9dªG,L2â\9d« ⊢ T2 ⁝ A.
#G #L1 #T1 #A #H elim H -G -L1 -T1 -A
[ #G #L1 #s1 #X #H1 elim (teqx_inv_sort1 … H1) -H1 //
| #I #G #L1 #V1 #B #_ #IH #X #H1 >(teqx_inv_lref1 … H1) -H1