Commit 9e00370c authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Fin preuve WfAx dans ZF.v

parent ad6cdeeb
......@@ -3,6 +3,7 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import ROmega.
Require Import Defs NameProofs Mix Meta Theories PreModels Models.
Import ListNotations.
Local Open Scope bool_scope.
......@@ -194,14 +195,13 @@ Proof.
simpl (Nat.max 1 _).
assert (H := level_lift_form_above C 1).
assert (H' := level_lift_form_above C 2).
admit.
(* omega with *. *)
romega with *.
+ apply nForall_fclosed. red. unfold Names.Empty. intro a. intro.
rewrite !aux2' in H. cbn -[Names.union] in H.
rewrite !fvars_lift_form_above in H.
unfold FClosed in HC'. unfold Names.Empty in HC'. destruct HC' with (a := a).
namedec.
Admitted.
Qed.
End ZFAx.
......
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