Commit 6b4d42fe authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

FsetInduction.Induction is valid whatever p, so change it to a lemma.

parent 874b3cf0
......@@ -229,7 +229,7 @@ theory FsetInduction
predicate p (set t)
axiom Induction :
lemma Induction :
(forall s: set t. is_empty s -> p s) ->
(forall s: set t. p s -> forall t: t.
not (mem t s) -> p (add t s)) ->
......
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