proposition: Lemma subst_comp_is_subst_comp_aux1 : forall v sigma f, find eq_var_bool v (map_subst f sigma) = match find eq_var_bool 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. reflexivity. generalize (X.eq_bool_ok v v1); case (eq_var_bool v v1). intro v_eq_v1; subst v1; reflexivity. intros _; apply IHsigma. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)