Require Export List.
Require Export Omega.

Module Type DecHerFinZF.

Parameter hf : Type.
Parameter IN : hf -> hf -> Prop.
Definition nIN (x y:hf) : Prop := ~IN x y.
Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).

Definition Subq (X Y:hf) : Prop := forall z, z ∈ X -> z ∈ Y.
Infix "⊆" := Subq (at level 70).

(*** Decidable Membership ***)
Parameter INb : hf -> hf -> bool.
Axiom IN_ref : forall x y, x ∈ y <-> INb x y = true.

(*** Extensionality ***)
Axiom set_ext : forall X Y, X ⊆ Y -> Y ⊆ X -> X = Y.

(*** Epsilon Induction (Foundation) ***)
Axiom eps_ind : forall (P:hf -> Prop), (forall X, (forall x, x ∈ X -> P x) -> P X) -> forall X, P X.

(*** Empty ***)
Parameter empty : hf.
Notation "∅" := empty.
Axiom emptyE : forall (x:hf), x ∉ ∅.

(*** Unordered Pairs ***)
Parameter upair : hf -> hf -> hf.
Notation "{ x , y }" := (upair x y).
Axiom upairAx : forall (x y z:hf), z ∈ {x,y} <-> z = x \/ z = y.

(*** Unions ***)
Parameter union : hf -> hf.
Notation "⋃" := union (at level 40).
Axiom unionAx : forall (x z:hf), z ∈ ⋃ x <-> exists y, y ∈ x /\ z ∈ y.

(*** Power Sets ***)
Parameter power : hf -> hf.
Notation "℘" := power.
Axiom powerAx : forall (X:hf), forall Y:hf, Y ⊆ X <-> Y ∈ ℘ X.

(*** Replacement (for functions) ***)
Parameter repl : hf -> (hf -> hf) -> hf.
Notation "{ f | x ⋳ X }" := (repl X (fun x:hf => f)).
Axiom replAx : forall X f z, z ∈ {f x|x ⋳ X} <-> exists x, x ∈ X /\ z = f x.

(*** Separation (for decidable properties) ***)
Parameter sep : hf -> (hf -> bool) -> hf.
Notation "{ x ⋳ X | P }" := (sep X (fun x:hf => P)).
Axiom sepAx : forall X P z, z ∈ {x ⋳ X|P x} <-> z ∈ X /\ P z = true.

End DecHerFinZF.

Module AckermannCoding1937 : DecHerFinZF.

Definition hf := nat.

Fixpoint mod2 (x:nat) : bool :=
match x with
| O => false
| S O => true
| S (S x') => mod2 x'
end.

Fixpoint div2 (x:nat) : nat :=
match x with
| O => O
| S O => O
| S (S x') => S (div2 x')
end.

Fixpoint mul2 (x:nat) : nat :=
match x with
| O => O
| S x' => S (S (mul2 x'))
end.

Lemma mod2S x : mod2 (S x) <> mod2 x.
induction x.
- simpl. discriminate.
- simpl. destruct x.
  + simpl. discriminate.
  + intros H1. apply IHx. symmetry. exact H1.
Qed.

Lemma S_even_odd x : mod2 x = false -> mod2 (S x) = true.
intros H1. case_eq (mod2 (S x)); intros H2; try reflexivity.
exfalso. apply (mod2S x). congruence.
Qed.

Lemma S_odd_even x : mod2 x = true -> mod2 (S x) = false.
intros H1. case_eq (mod2 (S x)); intros H2; try reflexivity.
exfalso. apply (mod2S x). congruence.
Qed.

Lemma mod2mul2 x : mod2 (mul2 x) = false.
induction x.
- reflexivity.
- simpl. exact IHx.
Qed.

Lemma mod2Smul2 x : mod2 (S (mul2 x)) = true.
induction x.
- reflexivity.
- simpl. exact IHx.
Qed.

Lemma div2mul2 x : div2 (mul2 x) = x.
induction x.
- reflexivity.
- simpl. congruence.
Qed.

Lemma div2Smul2 x : div2 (S (mul2 x)) = x.
induction x.
- reflexivity.
- simpl. f_equal. exact IHx.
Qed.

Lemma mod2div2S x : (mod2 x = true -> div2 (S x) = S (div2 x)) /\ (mod2 x = false -> div2 (S x) = div2 x).
induction x; split; intros H1.
- discriminate H1.
- reflexivity.
- case_eq (mod2 x); intros H2.
  + exfalso. apply (mod2S x). congruence.
  + destruct IHx. rewrite (H0 H2). simpl. reflexivity.
- case_eq (mod2 x); intros H2.
  + destruct IHx. rewrite (H H2). simpl. reflexivity.
  + exfalso. apply (mod2S x). congruence.
Qed.

Lemma mod2tdiv2S x : mod2 x = true -> div2 (S x) = S (div2 x).
generalize (mod2div2S x). tauto.
Qed.

Lemma mod2fdiv2S x : mod2 x = false -> div2 (S x) = div2 x.
generalize (mod2div2S x). tauto.
Qed.

Lemma mul2div2_evenodd x : (mod2 x = false /\ mul2 (div2 x) = x) \/ (mod2 x = true /\ S (mul2 (div2 x)) = x).
induction x.
- simpl. left. tauto.
- destruct IHx as [[IH1 IH2]|[IH1 IH2]].
  + rewrite (mod2fdiv2S x IH1). rewrite IH2. right. split; try reflexivity.
    now apply (S_even_odd x).
  + rewrite (mod2tdiv2S x IH1). left. split.
    * now apply (S_odd_even x).
    * simpl. rewrite IH2. reflexivity.
Qed.

Lemma mul2div2_even x : mod2 x = false -> mul2 (div2 x) = x.
destruct (mul2div2_evenodd x) as [[H1 H2]|[H1 H2]]; try tauto.
intros H. rewrite H in H1. discriminate.
Qed.

Lemma mul2div2_odd x : mod2 x = true -> S (mul2 (div2 x)) = x.
destruct (mul2div2_evenodd x) as [[H1 H2]|[H1 H2]]; try tauto.
intros H. rewrite H in H1. discriminate.
Qed.

Lemma div2mod2_eq x y : div2 x = div2 y -> mod2 x = mod2 y -> x = y.
case_eq (mod2 x); intros H1; case_eq (mod2 y); intros H2; try discriminate.
- intros H3 _. rewrite <- (mul2div2_odd x H1). rewrite <- (mul2div2_odd y H2). rewrite H3. reflexivity.
- intros H3 _. rewrite <- (mul2div2_even x H1). rewrite <- (mul2div2_even y H2). rewrite H3. reflexivity.
Qed.

Lemma complete_induction (P:nat -> Prop) :
(forall x, (forall y, y < x -> P y) -> P x) ->
(forall x, P x).
intros H x. apply H. induction x.
- intros y H1. omega.
- intros y H1. 
  assert (H2:y < x \/ y = x) by omega.
  destruct H2 as [H2|H2].
  + now apply IHx.
  + rewrite H2. apply H. exact IHx.
Qed.

Lemma div2SSlt x : div2 (S x) < S x /\ div2 (S (S x)) < S (S x).
induction x; split.
- simpl. omega.
- simpl. omega.
- tauto.
- change (S (div2 (S x)) < S (S (S x))). omega.
Qed.

Lemma div2Slt x : div2 (S x) < S x.
generalize (div2SSlt x). tauto.
Qed.

Lemma div2_induction (P:nat -> Prop) :
P 0 -> (forall x, P (div2 x) -> P x) ->
forall x, P x.
intros H1 H2. apply complete_induction.
intros [|x] H3.
- assumption.
- apply H2. apply H3. apply div2Slt.
Qed.

Fixpoint INb (x y:hf) : bool :=
match x with
| O => mod2 y
| S x' => INb x' (div2 y)
end.

Lemma div2INb x y : INb x (div2 y) = INb (S x) y.
reflexivity.
Qed.

Definition empty : hf := 0.

Lemma emptyEq : forall x, INb x empty = false.
induction x.
- reflexivity.
- simpl. exact IHx.
Qed.

Lemma INb_leq x y : INb x y = true -> x < y.
revert y. induction x.
- intros [|y].
  + simpl. discriminate.
  + omega.
- intros [|y] H1.
  + rewrite emptyEq in H1. discriminate.
  + rewrite <- div2INb in H1. apply IHx in H1.
    generalize (div2Slt y). omega.
Qed.

Fixpoint adj (x:nat) (y:nat) : nat :=
match x with
| O => if (mod2 y) then y else S y
| S x' => if (mod2 y) then S (mul2 (adj x' (div2 y))) else mul2 (adj x' (div2 y))
end.

(***
Compute (INb 0 0).
Compute (INb 0 (adj 0 0)).
Compute (INb (adj 0 0) (adj 0 0)).
Compute (adj 0 0).
Compute (adj (adj 0 0) (adj 0 0)).
Compute (adj 0 (adj (adj 0 0) 0)).
Compute (INb 0 (adj (adj 0 0) (adj 0 0))).
Compute (INb (adj 0 0) (adj (adj 0 0) (adj 0 0))).
***)

Lemma INbdiv2adj x y : div2 (adj (S x) y) = adj x (div2 y).
simpl. case_eq (mod2 y); intros H1.
- rewrite div2Smul2. reflexivity.
- rewrite div2mul2. reflexivity.
Qed.

Lemma adjEq : forall z x y, INb z (adj x y) = true <-> z = x \/ INb z y = true.
induction z.
- intros [|x] y; simpl.
  + case_eq (mod2 y); try tauto. intros H1. split; try tauto. intros _. case_eq (mod2 (S y)); try reflexivity. intros H2. exfalso. apply (mod2S y). congruence.
  + case_eq (mod2 y).
    * intros H1. split; try tauto. intros _. apply mod2Smul2.
    * intros H1. { split.
      - intros H2. rewrite mod2mul2 in H2. discriminate.
      - intros [H2|H2]; discriminate.
    }
- intros x y. rewrite <- div2INb. rewrite <- div2INb. destruct x.
  + simpl. case_eq (mod2 y); intros H1.
    * split; try tauto. intros [H2|H2]; try discriminate; tauto.
    * rewrite (mod2fdiv2S y H1). split; try tauto. intros [H2|H2]; try discriminate; tauto.
  + simpl. case_eq (mod2 y); intros H1.
    * rewrite div2Smul2. specialize (IHz x (div2 y)). { split.
      - intros H2. apply IHz in H2. destruct H2; try tauto. left. congruence.
      - intros [H2|H2]; try tauto. assert (E:z = x) by omega. tauto.
    }
    * rewrite div2mul2. specialize (IHz x (div2 y)). { split.
      - intros H2. apply IHz in H2. destruct H2; try tauto. left. congruence.
      - intros [H2|H2]; try tauto. assert (E:z = x) by omega. tauto.
    }
Qed.

Lemma adjINb x y : INb x y = true -> adj x y = y.
revert y. induction x; intros y.
- simpl. intros H1. rewrite H1. reflexivity.
- simpl. intros H1. rewrite (IHx (div2 y) H1).
  case_eq (mod2 y); intros H2.
  + now apply mul2div2_odd.
  + now apply mul2div2_even.
Qed.

Fixpoint list2hf (l:list nat) : nat :=
match l with
| nil => 0
| cons x r => adj x (list2hf r)
end.

Lemma INb_list2hf (l:list nat) : forall z, In z l <-> INb z (list2hf l) = true.
intros z. induction l; split; intros H1.
- inversion H1.
- simpl in H1. rewrite emptyEq in H1. discriminate H1.
- destruct H1.
  + rewrite H. simpl. apply adjEq. tauto.
  + simpl. apply adjEq. tauto.
- simpl in H1. apply adjEq in H1. simpl. destruct H1.
  + symmetry in H. tauto.
  + tauto.
Qed.

Lemma nat_remove_In_iff (x y:nat) l : In x (remove eq_nat_dec y l) <-> x <> y /\ In x l.
induction l; simpl; split; try tauto.
- intros H1. destruct (eq_nat_dec y a) as [H2|H2].
  + tauto.
  + destruct H1 as [H3|H3].
    * split; try tauto. congruence.
    * tauto.
- intros [H1 [H2|H2]].
  + destruct (eq_nat_dec y a) as [H3|H3]; try congruence. now left.
  + destruct (eq_nat_dec y a) as [H3|H3]; try tauto. right. tauto.
Qed.

Definition tmin m n := m - (m - n).

Fixpoint hf2list (x:nat) : list nat :=
match x with
| O => nil
| S x' => if mod2 x then (0::(map S (hf2list (tmin x' (div2 x))))) else (map S (hf2list (tmin x' (div2 x))))
end.

Lemma tmindiv2 x : tmin x (div2 (S x)) = div2 (S x) /\ tmin (S x) (div2 (S (S x))) = div2 (S (S x)).
induction x; split.
- simpl. reflexivity.
- simpl. reflexivity.
- tauto.
- change (tmin (S (S x)) (S (div2 (S x))) = S (div2 (S x))).
  destruct IHx as [IH _].
  unfold tmin in *|-*. omega.
Qed.

(***
Compute (hf2list 5).
Compute (hf2list 2).
Compute (hf2list 1).
***)

Lemma hf2list_eq (x:nat) : (mod2 x = true /\ hf2list x = (0::(map S (hf2list (div2 x))))) \/ (mod2 x = false /\ hf2list x = (map S (hf2list (div2 x)))).
induction x.
- right. simpl. tauto.
- destruct IHx as [[IH1 IH2]|[IH1 IH2]].
  + right. case_eq (mod2 (S x)); intros H1.
    * exfalso. apply (mod2S x); congruence.
    * split; try reflexivity.
      change ((if (mod2 (S x)) then (0::(map S (hf2list (tmin x (div2 (S x)))))) else (map S (hf2list (tmin x (div2 (S x)))))) = map S (hf2list (div2 (S x)))).
      rewrite H1. destruct (tmindiv2 x) as [H2 _]. rewrite H2. reflexivity.
  + left. case_eq (mod2 (S x)); intros H1.
    * split; try reflexivity.
      change ((if (mod2 (S x)) then (0::(map S (hf2list (tmin x (div2 (S x)))))) else (map S (hf2list (tmin x (div2 (S x)))))) = 0::(map S (hf2list (div2 (S x))))).
      rewrite H1. destruct (tmindiv2 x) as [H2 _]. rewrite H2. reflexivity.
    * exfalso. apply (mod2S x); congruence.
Qed.

Lemma hf2list_t_eq (x:nat) : mod2 x = true -> hf2list x = (0::(map S (hf2list (div2 x)))).
destruct (hf2list_eq x) as [[H1 H2]|[H1 H2]]; try tauto.
intros H. rewrite H in H1. discriminate.
Qed.

Lemma hf2list_f_eq (x:nat) : mod2 x = false -> hf2list x = (map S (hf2list (div2 x))).
destruct (hf2list_eq x) as [[H1 H2]|[H1 H2]]; try tauto.
intros H. rewrite H in H1. discriminate.
Qed.

Lemma list2hf_mapS_even l : mod2 (list2hf (map S l)) = false.
induction l.
- reflexivity.
- simpl. rewrite IHl. apply mod2mul2.
Qed.

Lemma list2hf_mapS (l:list nat) : list2hf (map S l) = mul2 (list2hf l).
induction l.
- reflexivity.
- simpl. rewrite list2hf_mapS_even.
  f_equal. f_equal. rewrite IHl. apply div2mul2.
Qed.

Lemma list2hf_hf2list (x:nat) : list2hf (hf2list x) = x.
revert x. apply div2_induction.
- simpl. reflexivity.
- intros x H1. destruct (hf2list_eq x) as [[H2 H3]|[H2 H3]].
  + rewrite H3. simpl. rewrite list2hf_mapS_even. rewrite list2hf_mapS. rewrite H1. now rewrite mul2div2_odd.
  + rewrite H3. rewrite list2hf_mapS. rewrite H1. now rewrite mul2div2_even.
Qed.

Lemma INb_hf2list z y : INb z y = true <-> In z (hf2list y).
revert y z. apply (div2_induction (fun y => forall z, INb z y = true <-> In z (hf2list y))).
- intros z. split.
  + intros H1. rewrite emptyEq in H1. discriminate H1.
  + simpl. intros [].
- intros y IH z. split.
  + intros H1. destruct z; simpl in H1.
    * rewrite (hf2list_t_eq y H1). left. reflexivity.
    * { destruct (hf2list_eq y) as [[H2 H3]|[H2 H3]].
      - rewrite H3. simpl.
        right. apply in_map. apply IH. exact H1.
      - rewrite H3. apply in_map. apply IH. exact H1.
      }
  + intros H1. destruct (hf2list_eq y) as [[H2 H3]|[H2 H3]].
    * rewrite H3 in H1. { destruct H1 as [H1|H1].
      - rewrite <- H1. exact H2.
      - apply in_map_iff in H1. destruct H1 as [x [H4 H5]].
        rewrite <- H4. simpl. apply IH. assumption.
      }
    * rewrite H3 in H1. apply in_map_iff in H1. destruct H1 as [x [H4 H5]].
      rewrite <- H4. simpl. apply IH. assumption.
Qed.    

Definition equi (l1 l2:list nat) := incl l1 l2 /\ incl l2 l1.

Lemma hf2list_list2hf (l:list nat) : equi (hf2list (list2hf l)) l.
induction l.
- simpl. split; now apply incl_refl.
- simpl. split.
  + intros z H1. apply INb_hf2list in H1. apply adjEq in H1.
    destruct H1 as [H1|H1].
    * left. congruence.
    * right. apply IHl. apply INb_hf2list. assumption.
  + intros z [H1|H1].
    * rewrite H1. apply INb_hf2list. apply adjEq. tauto.
    * apply INb_hf2list. apply adjEq. right. apply IHl in H1. apply INb_hf2list in H1. assumption.
Qed.

Lemma empty_or_nonempty y : y = 0 \/ exists x, INb x y = true.
revert y. apply (div2_induction (fun y => y = 0 \/ exists x, INb x y = true)).
- left. reflexivity.
- intros y [IH|[x IH]].
  + destruct y; try tauto. destruct y.
    * right. exists 0. reflexivity.
    * simpl in IH. discriminate IH.
  + right. exists (S x). rewrite <- div2INb. assumption.
Qed.

Lemma INb_ext (x y:hf) : (forall z, INb z x = true <-> INb z y = true) -> x = y.
revert x y. apply (div2_induction (fun x => forall y, (forall z, INb z x = true <-> INb z y = true) -> x = y)).
- intros [|y]; try tauto.
  intros H1. exfalso. destruct (empty_or_nonempty (S y)) as [H2|[z H2]].
  + discriminate H2.
  + apply H1 in H2. rewrite emptyEq in H2. discriminate H2.
- intros x IHx y H1.
  specialize (IHx (div2 y)).
  assert (E1:div2 x = div2 y). {
    apply IHx. intros z. rewrite div2INb. rewrite div2INb. apply H1.
  }
  assert (E2:mod2 x = mod2 y). {
    case_eq (mod2 x); intros H2; case_eq (mod2 y); intros H3; try congruence.
    - exfalso. specialize (H1 0). simpl in H1. apply H1 in H2. congruence.
    - exfalso. specialize (H1 0). simpl in H1. apply H1 in H3. congruence.
  }
  now apply div2mod2_eq.
Qed.

Definition IN (x y:hf) : Prop := INb x y = true.
Definition nIN (x y:hf) : Prop := ~IN x y.

Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).

Definition Subq (X Y:hf) : Prop := forall z, z ∈ X -> z ∈ Y.
Infix "⊆" := Subq (at level 70).

(*** Reflection (trivial by definition of IN) ***)
Lemma IN_ref : forall x y, x ∈ y <-> INb x y = true.
unfold IN. tauto.
Qed.

(*** Set Extensionality ***)
Lemma set_ext : forall X Y, X ⊆ Y -> Y ⊆ X -> X = Y.
intros X Y H1 H2. apply INb_ext. intros z. split.
- apply H1.
- apply H2.
Qed.

(*** Epsilon Induction ***)
Lemma eps_ind (P:hf -> Prop) : (forall X, (forall x, x ∈ X -> P x) -> P X) -> forall X, P X.
intros H1. apply complete_induction.
intros X H2. apply H1. intros x H3. apply H2.
unfold IN in H3. now apply INb_leq.
Qed.

Notation "∅" := empty.

Lemma emptyE (x:hf) : x ∉ ∅.
unfold nIN. unfold IN. rewrite emptyEq. discriminate.
Qed.

Definition upair (x y:hf) : hf := list2hf (x::y::nil).

Notation "{ x , y }" := (upair x y).

Lemma upairAx (x y z:hf) : z ∈ {x,y} <-> z = x \/ z = y.
unfold upair. simpl. unfold IN. split.
- intros H1. rewrite adjEq in H1. destruct H1 as [H1|H1]; try tauto.
  rewrite adjEq in H1. destruct H1 as [H1|H1]; try tauto.
  rewrite emptyEq in H1. discriminate H1.
- intros H1. apply adjEq. destruct H1 as [H1|H1]; try tauto.
  right. apply adjEq. tauto.
Qed.

Definition union (x:hf) : hf := list2hf (flat_map hf2list (hf2list x)).

Notation "⋃" := union (at level 40).

Lemma unionAx (x z:hf) : z ∈ ⋃ x <-> exists y, y ∈ x /\ z ∈ y.
unfold union, IN. split.
- intros H1. apply INb_list2hf in H1. apply in_flat_map in H1. destruct H1 as [y [H2 H3]].
  exists y. apply INb_hf2list in H2. apply INb_hf2list in H3. tauto.
- intros [y [H2 H3]]. apply INb_list2hf. apply in_flat_map.
  exists y. split; now apply INb_hf2list.
Qed.

Definition repl (X:hf) (f:hf -> hf) : hf := list2hf (map f (hf2list X)).

Notation "{ f | x ⋳ X }" := (repl X (fun x:hf => f)).

Lemma replAx X f z : z ∈ {f x|x ⋳ X} <-> exists x, x ∈ X /\ z = f x.
unfold repl. unfold IN. split; intros H1.
- apply INb_list2hf in H1. apply in_map_iff in H1. destruct H1 as [x [H2 H3]].
  exists x. split; try congruence. apply INb_hf2list in H3. assumption.
- destruct H1 as [x [H2 H3]]. apply INb_list2hf. apply in_map_iff. exists x.
  split; try congruence. apply INb_hf2list. assumption.
Qed.

Definition sep (X:hf) (P:hf -> bool) : hf := list2hf (filter P (hf2list X)).

Notation "{ x ⋳ X | P }" := (sep X (fun x:hf => P)).

Lemma sepAx X P z : z ∈ {x ⋳ X|P x} <-> z ∈ X /\ P z = true.
unfold sep, IN. split.
- intros H1. apply INb_list2hf in H1. apply filter_In in H1. split; try tauto. apply INb_hf2list. tauto.
- intros [H1 H2]. apply INb_list2hf. apply filter_In. split; try tauto. apply INb_hf2list. tauto.
Qed.

(*** Is the other version of replacement provable? Probably not if the relation goes to Prop. ***)
Fixpoint powerl (l:list hf) : list hf :=
match l with
| (x::r) => powerl r ++ map (adj x) (powerl r)
| nil => cons 0 nil
end.

Definition power (X:hf) : hf := list2hf (powerl (hf2list X)).

Notation "℘" := power.

Lemma powerl_lem (l:list hf) : forall Y:hf, Y ⊆ list2hf l <-> In Y (powerl l).
unfold Subq. unfold IN. induction l.
- intros Y. split; intros H1.
  + simpl in H1. simpl. destruct (empty_or_nonempty Y) as [H2|[y H2]].
    * left. congruence.
    * exfalso. apply H1 in H2. rewrite emptyEq in H2. discriminate H2.
  + intros z H2. simpl in H1. destruct H1 as [H1|[]].
    exfalso. rewrite <- H1 in H2. rewrite emptyEq in H2. discriminate H2.
- intros Y. split; intros H1.
  + simpl. apply in_or_app. case_eq (INb a Y); intros H2.
    * right. apply in_map_iff.
      exists (list2hf (remove eq_nat_dec a (hf2list Y))).
      { split.
        - apply INb_ext. intros z. split; intros H3.
          + apply adjEq in H3. destruct H3 as [H3|H3].
            * rewrite H3. assumption.
            * apply INb_list2hf in H3. apply nat_remove_In_iff in H3. destruct H3 as [_ H4]. apply INb_hf2list in H4. assumption.
          + apply adjEq. destruct (eq_nat_dec z a) as [H4|H4]; try tauto.
            right. apply INb_list2hf. apply nat_remove_In_iff. split; try assumption. apply INb_hf2list in H3. assumption.
        - apply IHl. intros z H3. apply INb_list2hf in H3. apply nat_remove_In_iff in H3. destruct H3 as [H4 H5].
          apply INb_hf2list in H5. apply H1 in H5. simpl in H5. apply adjEq in H5. tauto.
      }
    * left. apply IHl. intros z H3. generalize (H1 z H3). intros H4. simpl in H4. apply adjEq in H4. destruct H4 as [H4|H4]; try tauto.
      rewrite H4 in H3. rewrite H2 in H3. discriminate.
  + intros z H2. simpl in H1. apply in_app_or in H1. destruct H1 as [H1|H1].
    * simpl. destruct (IHl Y) as [IH1 IH2]. specialize (IH2 H1 z H2). apply adjEq. tauto.
    * simpl. apply adjEq.
      destruct (eq_nat_dec z a) as [H3|H3]; try tauto. right.
      apply in_map_iff in H1. destruct H1 as [X [H4 H5]].
      destruct (IHl X) as [IH1 IH2].
      apply IH2; try assumption.
      rewrite <- H4 in H2. apply adjEq in H2. tauto.
Qed.

Lemma powerAx (X:hf) : forall Y:hf, Y ⊆ X <-> Y ∈ ℘ X.
unfold power. unfold IN. intros Y. generalize (powerl_lem (hf2list X) Y).
rewrite list2hf_hf2list. intros H1. split; intros H2.
- apply INb_list2hf. tauto.
- apply INb_list2hf in H2. tauto.
Qed.

End AckermannCoding1937.