proposition: Theorem silly3' : forall (n : nat), (beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true) -> true = beq_nat n 5 -> true = beq_nat (S (S n)) 7.
proof: Proof. MProof. intros n eq H. symmetry_in H. apply_in eq H. symmetry_in H. apply H. Qed.