include "basic_2/static/lsubf.ma".
-axiom lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
- ∀x2,y2. x2⋓y2 ≡ f2 →
- ∃∃x1,y1. ⦃L1, x1⦄ ⫃𝐅* ⦃L2, x2⦄ & ⦃L1, y1⦄ ⫃𝐅* ⦃L2, y2⦄ & x1⋓y1 ≡ f1.
-
(* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
(* Properties with context-sensitive free variables *************************)
| /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/