proposition: Lemma subst_envs_comp_cons : forall G, subst_envs_comp G -> subst_envs_comp (None :: G).
proof: Proof. intros. intros i j Ti Tj Gi Gj. destruct i; destruct j. try_solve. inversion Gi. inversion Gj. apply (H i j). inversion Gi; trivial. inversion Gj; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)