proposition: Lemma subst_ran_cons_some t G : subst_ran (Some t::G) = env t [+] subst_ran G.
proof: Proof. unfold subst_ran. simpl. destruct (env t). rewrite env_sum_empty_l; trivial. simpl. rewrite fold_subst_ran. set (f := fun E S => match S with Some T => E[+]env T | None => E end). fold EmptyEnv. destruct (fold_left f G EmptyEnv). rewrite env_sum_empty_r; trivial. destruct o0; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)