proposition: Theorem plus_n_n_injective : forall n m, n + n = m + m -> n = m.
proof: Proof. MProof. intros n. elim n &> [i:~~| \n']. Admitted. Theorem double_injective_FAILED : forall n m, double n = double m -> n = m. MProof. intros n m. elim n &> [i:~~ | \n']. - simpl. destruct m &> [i: ~~ | \m'] &> intro eq. + reflexivity. + inversion eq. - destruct m &> [i:~~ | \m'] &> intro IH &> intro eq. + inversion eq. + apply f_equal. Abort. Theorem double_injective : forall n m, double n = double m -> n = m. MProof. intros n. elim n &> [i: ~~| \n' IH]. - simpl. destructn 0 &> [i:~~| \m'] &> intro eq. + reflexivity. + inversion eq. - simpl. destructn 0 &> [i:~~ | \m'] &> intro eq. + simpl. inversion eq. + apply f_equal. apply IH. inversion eq. reflexivity. Qed.