1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/static/lsubf.ma".
17 axiom lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
19 ∃∃x1,y1. ⦃L1, x1⦄ ⫃𝐅* ⦃L2, x2⦄ & ⦃L1, y1⦄ ⫃𝐅* ⦃L2, y2⦄ & x1⋓y1 ≡ f1.
21 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
23 (* Properties with context-sensitive free variables *************************)
25 lemma lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 →
26 ∀f1,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 ⊢ 𝐅*⦃T⦄ ≡ f1.
27 #f2 #L2 #T #H elim H -f2 -L2 -T
28 [ /3 width=5 by lsubf_fwd_isid_dx, frees_sort/
29 | #f2 #i #Hf2 #g1 #Y1 #H
30 elim (lsubf_inv_atom2 … H) -H #Hg1 #H destruct
31 elim (eq_inv_pushs_dx … Hg1) -Hg1 #g #Hg #H destruct
32 elim (eq_inv_xn … Hg) -Hg
33 /3 width=3 by frees_atom, isid_eq_repl_fwd/
34 | #f2 #I #K2 #W #_ #IH #g1 #Y1 #H elim (lsubf_inv_pair2 … H) -H *
35 [ #f1 #K1 #H12 #H1 #H2 destruct /3 width=1 by frees_pair/
36 | #f #f0 #f1 #K1 #V #H12 #Hf #Hf1 #H1 #H2 #H3 destruct
37 /4 width=5 by frees_pair, frees_flat/
39 | #f2 #I #L2 #Hf2 #g1 #Y1 #H elim (lsubf_inv_unit2 … H) -H *
40 [ #f1 #L1 #H12 #H1 #H2 destruct
41 /3 width=5 by lsubf_fwd_isid_dx, frees_unit/
42 | #f #f0 #f1 #J #L1 #V #H12 #Hf #Hf1 #H1 #H2 destruct
43 /5 width=9 by lsubf_fwd_isid_dx, frees_eq_repl_back, frees_pair, sor_isid_inv_sn/
45 | #f2 #I #L2 #i #_ #IH #g1 #L1 #H elim (lsubf_inv_push2 … H) -H
46 /3 width=1 by frees_lref/
47 | /3 width=5 by lsubf_fwd_isid_dx, frees_gref/
48 | #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
49 elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 #f1V #g1T #HV #HT #Hf1
50 elim (lsubf_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct
51 /3 width=5 by frees_bind/
52 | #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12
53 elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 /3 width=5 by frees_flat/