proposition: Lemma subst_envs_comp_head a : forall G, subst_envs_comp (Some a::G) -> env a [<->] subst_ran G.
proof: Proof. induction G. intros; apply env_comp_empty. intros envsc. assert (se: subst_envs_comp (Some a :: G)). intros p q Ti Tj A B. destruct p. destruct q; try tauto. inversion A; inversion B; rewrite <- H0; rewrite <- H1; apply env_comp_refl. apply (envsc 0 (S (S q))); try_solve. destruct q. apply (envsc (S (S p)) 0); try_solve. apply (envsc (S (S p)) (S (S q))); try_solve. destruct a0. rewrite subst_ran_cons_some. apply env_comp_sum. apply (envsc 0 1); try_solve. apply IHG; trivial. rewrite subst_ran_cons_none. apply IHG; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)