proposition: Theorem beq_nat_true : forall n m, beq_nat n m = true -> n = m.
proof: Proof. MProof. Admitted. Theorem double_injective_take2_FAILED : forall n m, double n = double m -> n = m. MProof. intros n m. elim m &> [i:~~ | \m']. - simpl. destruct n &> [i:~~ | \n'] &> intro eq. + reflexivity. + inversion eq. - destruct n &> [i:~~| \n'] &> intro IH &> intro eq. + inversion eq. + apply f_equal. Abort. Local Definition tac := destructn 0 &> [i:~~| \n'] &> intro eq. Theorem double_injective_take2 : forall n m, double n = double m -> n = m. MProof. intros n m. move_back n. elim m &> [i:~~| \m' IHm']. - simpl. tac. + reflexivity. + inversion eq. - tac. + inversion eq. + apply f_equal. apply IHm'. inversion eq. reflexivity. Qed.