include "ground_2/relocation/rtmap_uni.ma".
include "basic_2/notation/relations/relation_3.ma".
include "basic_2/syntax/cext2.ma".
include "ground_2/relocation/rtmap_uni.ma".
include "basic_2/notation/relations/relation_3.ma".
include "basic_2/syntax/cext2.ma".
(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************)
definition lex (R): relation lenv ≝
(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************)
definition lex (R): relation lenv ≝
- λL1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤*[cfull, cext2 R, f] L2.
+ λL1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤[cfull, cext2 R, f] L2.
lemma lex_bind (R): ∀I1,I2,K1,K2. K1 ⪤[R] K2 → cext2 R K1 I1 I2 →
K1.ⓘ{I1} ⪤[R] K2.ⓘ{I2}.
#R #I1 #I2 #K1 #K2 * #f #Hf #HK12 #HI12
lemma lex_bind (R): ∀I1,I2,K1,K2. K1 ⪤[R] K2 → cext2 R K1 I1 I2 →
K1.ⓘ{I1} ⪤[R] K2.ⓘ{I2}.
#R #I1 #I2 #K1 #K2 * #f #Hf #HK12 #HI12
lemma lex_co (R1) (R2): (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
∀L1,L2. L1 ⪤[R1] L2 → L1 ⪤[R2] L2.
lemma lex_co (R1) (R2): (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
∀L1,L2. L1 ⪤[R1] L2 → L1 ⪤[R2] L2.
qed-.
lemma lex_inv_bind_sn (R): ∀I1,L2,K1. K1.ⓘ{I1} ⪤[R] L2 →
∃∃I2,K2. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L2 = K2.ⓘ{I2}.
#R #I1 #L2 #K1 * #f #Hf #H
qed-.
lemma lex_inv_bind_sn (R): ∀I1,L2,K1. K1.ⓘ{I1} ⪤[R] L2 →
∃∃I2,K2. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L2 = K2.ⓘ{I2}.
#R #I1 #L2 #K1 * #f #Hf #H
-lapply (lexs_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
-elim (lexs_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
+lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+elim (sex_inv_push1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
/3 width=5 by ex2_intro, ex3_2_intro/
qed-.
(* Basic_2A1: was: lpx_sn_inv_atom2 *)
lemma lex_inv_atom_dx (R): ∀L1. L1 ⪤[R] ⋆ → L1 = ⋆.
/3 width=5 by ex2_intro, ex3_2_intro/
qed-.
(* Basic_2A1: was: lpx_sn_inv_atom2 *)
lemma lex_inv_atom_dx (R): ∀L1. L1 ⪤[R] ⋆ → L1 = ⋆.
qed-.
lemma lex_inv_bind_dx (R): ∀I2,L1,K2. L1 ⪤[R] K2.ⓘ{I2} →
∃∃I1,K1. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L1 = K1.ⓘ{I1}.
#R #I2 #L1 #K2 * #f #Hf #H
qed-.
lemma lex_inv_bind_dx (R): ∀I2,L1,K2. L1 ⪤[R] K2.ⓘ{I2} →
∃∃I1,K1. K1 ⪤[R] K2 & cext2 R K1 I1 I2 & L1 = K1.ⓘ{I1}.
#R #I2 #L1 #K2 * #f #Hf #H
-lapply (lexs_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
-elim (lexs_inv_push2 … H) -H #I1 #K1 #HK12 #HI12 #H destruct
+lapply (sex_eq_repl_fwd … H (⫯f) ?) -H /2 width=1 by eq_push_inv_isid/ #H
+elim (sex_inv_push2 … H) -H #I1 #K1 #HK12 #HI12 #H destruct