proposition: Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2, split l = (l1, l2) -> combine l1 l2 = l.
proof: Proof. MProof. Admitted. Definition sillyfun1 (n : nat) : bool := if beq_nat n 3 then true else if beq_nat n 5 then true else false. Theorem sillyfun1_odd_FAILED : forall (n : nat), sillyfun1 n = true -> oddb n = true. MProof. intros n eq. unfold_in sillyfun1 eq. destruct (beq_nat n 3). Abort. Theorem sillyfun1_odd : forall (n : nat), sillyfun1 n = true -> oddb n = true. MProof. intros n. unfold sillyfun1. destruct_eq (beq_nat _ 3) &> intro Heqe3. - simpl. T.apply_in (beq_nat_true _ _) Heqe3. rewrite -> Heqe3. reflexivity. - destruct_eq (beq_nat _ _) &> intro Heqe5. + T.apply_in (beq_nat_true _ _) Heqe5. rewrite -> Heqe5. reflexivity. + intro eq. inversion eq. Qed.