proposition: Lemma make_conj_rapp : forall A eval l1 l2, @make_conj A eval (l1 +++ l2) <-> @make_conj A eval (l1++l2).
proof: Proof. intros A eval l1; induction l1 as [|? ? IHl1]. - simpl. tauto. - intros. simpl rev_append at 1. rewrite IHl1. rewrite make_conj_app. rewrite make_conj_cons. simpl app. rewrite make_conj_cons. rewrite make_conj_app. tauto. Qed.
imports: List