proposition: Lemma make_conj_app : forall A eval l1 l2, @make_conj A eval (l1 ++ l2) <-> @make_conj A eval l1 /\ @make_conj A eval l2.
proof: Proof. intros A eval l1; induction l1 as [|a l1 IHl1]. - simpl. tauto. - intros l2. change ((a::l1) ++ l2) with (a :: (l1 ++ l2)). rewrite make_conj_cons. rewrite IHl1. rewrite make_conj_cons. tauto. Qed.
imports: List