proposition: Lemma singleton_subst_active_aux : forall El Er El' Er' E i, (forall j, j <> i -> env_comp_on E El j) -> (forall j, j <> i -> env_comp_on E Er j) -> (forall j A, j <> i -> (El |= j := A <-> El' |= j := A)) -> (forall j A, j <> i -> (Er |= j := A <-> Er' |= j := A)) -> El' [<->] Er' -> El |= i :! -> Er |= i :! -> El [+] E [+] Er [=] (initialSeg (El' [+] Er') i ++ None :: finalSeg (El' [+] Er') (S i)) [+] E.
proof: Proof. intros. apply env_eq_def; intros j A. destruct (eq_nat_dec i j). rewrite <- e. split; intro D. destruct (env_sum_varDecl (El[+]E) Er D) as [[D' _] | D']. destruct (env_sum_varDecl El E D') as [[D'' _] | D'']. exfalso; apply varD_UD_absurd with El i A; trivial. apply env_sum_ry; trivial. exfalso; apply varD_UD_absurd with Er i A; trivial. apply env_sum_ly_rn; trivial. apply env_sum_ry. destruct (env_sum_varDecl (initialSeg (El'[+]Er') i ++ None :: finalSeg (El'[+]Er') (S i)) E D) as [[D' _] | D']; trivial. exfalso; apply (varD_UD_absurd D'). apply varUD_hole. assert (j <> i); [lia | idtac]. split; intro D. destruct (env_sum_varDecl (El[+]E) Er D) as [[D' Dn] | D']. destruct (env_sum_varDecl El E D') as [[D'' Dn'] | D'']. apply env_sum_ly_rn; trivial. apply varD_hole; trivial. apply env_sum_ly; trivial. apply (proj1 (H1 j A H6)); trivial. apply env_sum_ry; trivial. destruct (isVarDecl_dec E j) as [[B Ej] | En]. apply env_sum_ry. rewrite <- (H0 j H6 B); trivial. apply env_sum_ly. intros B C D1 D2. exfalso; apply varD_UD_absurd with E j C; trivial. apply varD_hole; trivial. apply env_sum_ry. apply (proj1 (H2 j A H6)); trivial. destruct (env_sum_varDecl (initialSeg (El'[+]Er') i ++ None :: finalSeg (El'[+]Er') (S i)) E D) as [[D' _] | D']. set (El'Er' := env_hole_subset (El'[+]Er') i D'). destruct (env_sum_varDecl El' Er' El'Er') as [[D'' Dn] | D'']. apply env_sum_ly. intros B C D1 D2. destruct (env_sum_varDecl El E D1) as [[D1l _] | D1r]. apply (H3 j B C). apply H1; hyp. apply H2; hyp. apply (H0 j H6); trivial. apply env_sum_ly. apply env_comp_on_sym. apply H; trivial. apply (proj2 (H1 j A H6)); trivial. apply env_sum_ry. apply (proj2 (H2 j A H6)); trivial. destruct (isVarDecl_dec Er j) as [[B D''] | Ern]. rewrite (H0 j H6 A B D' D''). apply env_sum_ry; trivial. apply env_sum_ly_rn; trivial. apply env_sum_ry; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)