proposition: Lemma envSubst_extend : forall i Q E, (forall j, ~envSub Q i j) -> exists Q', Q' |=> Q /\ exists j, envSub Q' i j /\ E |= j :! /\ (forall k l, envSub Q' k l -> (k <> i \/ l <> j) -> envSub Q k l).
proof: Proof. intros. set (v := max (size Q) (max i (length E))). set (f := fun x y => (x = i /\ y = v) \/ (envSub Q x y)). assert (f_dec: forall i j, {f i j} + {~f i j}). intros p q. destruct (envSub_dec Q p q). fo. destruct (eq_nat_dec p i); destruct (eq_nat_dec q v); subst; unfold f; tauto. assert (f_Lok: forall i j j', f i j -> f i j' -> j = j'). unfold f; intros. destruct H0; destruct H1. lia. absurd (envSub Q i0 j'); trivial. destruct H0; rewrite H0; fo. absurd (envSub Q i0 j); trivial. destruct H1; rewrite H1; fo. apply (envSub_Lok Q i0); trivial. assert (f_Rok: forall i i' j, f i j -> f i' j -> i = i'). unfold f; intros. destruct H0; destruct H1. lia. absurd (j < size Q). destruct H0; rewrite H2. unfold v; intro w. set (w' := Nat.le_max_l (size Q) (max i (length E))); lia. set (w := sizeOk Q i' j H1); fo. absurd (j < size Q). destruct H1; rewrite H2. unfold v; intro w. set (w' := Nat.le_max_l (size Q) (max i (length E))); lia. set (w := sizeOk Q i0 j H0); fo. apply (envSub_Rok Q) with j; trivial. assert (s_ok: forall i j, f i j -> i < S v /\ j < S v). intros. destruct H0 as [[i0_i jv] | x]; unfold v. rewrite jv; rewrite i0_i; split; auto. lia. destruct (sizeOk Q i0 j x). split; eauto with arith. exists (build_envSub f f_dec f_Lok f_Rok s_ok). simpl; split. fo. exists v; split. fo. split. constructor; apply nth_beyond. unfold v; eauto with arith. fo. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)