proposition: Lemma subst_comp_is_subst_comp_aux1 : forall v sigma f, find eq_variable_dec v (map_subst f sigma) = match find eq_variable_dec v sigma with | None => None | Some t => Some (f v t) end.
proof: Proof. intros v sigma f; induction sigma as [ | [v1 a1] sigma ]. simpl; trivial. simpl; elim (eq_variable_dec v v1); intro v_eq_v1; trivial; subst v; trivial. Qed.
imports: List more_list list_permut list_set Arith