proposition: Lemma fold_subst_ran : forall G l (f := fun E S => match S with Some T => E[+]env T | None => E end), fold_left f G l = l [+] fold_left f G nil.
proof: Proof. induction G. intros; simpl. rewrite env_sum_empty_r; trivial. intros l f. destruct a. simpl; destruct (env t). rewrite env_sum_empty_r. apply IHG. rewrite IHG; fold f. unfold f; rewrite (IHG (o::e)); fold f. rewrite env_sum_assoc; trivial. simpl; apply IHG. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)