(* Properties with context-sensitive free variables *************************)
-lemma lsubf_frees_trans: â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 →
- â\88\80f1,L1. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83L2, f2â¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f1.
+lemma lsubf_frees_trans: â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 →
+ â\88\80f1,L1. â¦\83L1, f1â¦\84 â«\83ð\9d\90\85* â¦\83L2, f2â¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f1.
#f2 #L2 #T #H elim H -f2 -L2 -T
[ /3 width=5 by lsubf_fwd_isid_dx, frees_sort/
| #f2 #i #Hf2 #g1 #Y1 #H
| /3 width=5 by lsubf_fwd_isid_dx, frees_gref/
| #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 #f1V #g1T #HV #HT #Hf1
- elim (lsubf_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct
+ elim (lsubf_bind_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct
/3 width=5 by frees_bind/
| #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 /3 width=5 by frees_flat/