proposition: Theorem injection_ex1 : forall (n m o : nat), [n;m] = [o;o] -> n = m.
proof: Proof. intros n m o H. Admitted. Theorem discriminate_ex1 : forall (n m : nat), false = true -> n = m. Proof. intros n m contra. discriminate contra. Qed.