(* Properties with context-sensitive free variables *************************)
lemma lsubf_frees_trans:
- â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f2 →
- â\88\80f1,L1. â¦\83L1,f1â¦\84 â«\83ð\9d\90\85+ â¦\83L2,f2â¦\84 â\86\92 L1 â\8a¢ ð\9d\90\85+â¦\83Tâ¦\84 ≘ f1.
+ â\88\80f2,L2,T. L2 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f2 →
+ â\88\80f1,L1. â\9dªL1,f1â\9d« â«\83ð\9d\90\85+ â\9dªL2,f2â\9d« â\86\92 L1 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ 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
elim (lsubf_inv_atom2 … H) -H #Hg1 #H destruct
- elim (eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct
+ elim (pr_eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct
elim (eq_inv_xn … Hg) -Hg
- /3 width=3 by frees_atom, isid_eq_repl_fwd/
+ /3 width=3 by frees_atom, pr_isi_eq_repl_fwd/
| #f2 #I #K2 #W #_ #IH #g1 #Y1 #H elim (lsubf_inv_pair2 … H) -H *
[ #f1 #K1 #H12 #H1 #H2 destruct /3 width=1 by frees_pair/
| #f #f0 #f1 #K1 #V #H12 #Hf #Hf1 #H1 #H2 #H3 destruct
[ #f1 #L1 #H12 #H1 #H2 destruct
/3 width=5 by lsubf_fwd_isid_dx, frees_unit/
| #f #f0 #f1 #J #L1 #V #H12 #Hf #Hf1 #H1 #H2 destruct
- /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, sor_isid_inv_sn/
+ /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, pr_sor_inv_isi_sn/
]
| #f2 #I #L2 #i #_ #IH #g1 #L1 #H elim (lsubf_inv_push2 … H) -H
/3 width=1 by frees_lref/