Commit d28c98b8 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Fin de la preuve du théorème de commutativité de +.

parent e89e640b
......@@ -296,6 +296,7 @@ Proof.
thm.
rec.
set (Γ' := _ :: _ :: Γ).
+
(** A Coq model of this Peano theory, based on the [nat] type *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment