diff --git a/CONFIG b/CONFIG
index 3a736fd..cf3cb85 100755
--- a/CONFIG
+++ b/CONFIG
@@ -1,2 +1,2 @@
 #!/bin/sh
-hol2dk config hol_upto_real.ml HOLLight_Real_With_N logic.v mappings.v BinNat deps.mk erasing.lp
+hol2dk config hol_upto_real.ml HOLLight_Real_With_N mappings.v BinNat deps.mk mappings.lp
diff --git a/logic.v b/logic.v
deleted file mode 100644
index b546b9e..0000000
--- a/logic.v
+++ /dev/null
@@ -1,619 +0,0 @@
-(****************************************************************************)
-(* Coq theory for encoding HOL-Light proofs. *)
-(****************************************************************************)
-
-Lemma ext_fun {A B} {f g : A -> B} : f = g -> forall x, f x = g x.
-Proof. intros fg x. rewrite fg. reflexivity. Qed.
-
-Lemma eq_false_negb_true b : b = false -> negb b = true.
-Proof. intro e. subst. reflexivity. Qed.
-
-(****************************************************************************)
-(* Type of non-empty types, used to interpret HOL-Light types types. *)
-(****************************************************************************)
-
-Record Type' := { type :> Type; el : type }.
-
-Definition bool' := {| type := bool; el := true |}.
-Canonical bool'.
-
-Definition Prop' : Type' := {| type := Prop; el := True |}.
-Canonical Prop'.
-
-Definition arr a (b : Type') := {| type := a -> b; el := fun _ => el b |}.
-Canonical arr.
-
-(****************************************************************************)
-(* Curryfied versions of some Coq connectives. *)
-(****************************************************************************)
-
-Definition imp (p q : Prop) : Prop := p -> q.
-
-Definition ex1 : forall {A : Type'}, (A -> Prop) -> Prop := fun A P => exists! x, P x.
-
-(****************************************************************************)
-(* Proof of some HOL-Light rules. *)
-(****************************************************************************)
-
-Lemma MK_COMB {a b : Type} {s t : a -> b} {u v : a} (h1 : s = t) (h2 : u = v)
-  : (s u) = (t v).
-Proof. rewrite h1, h2. reflexivity. Qed.
-
-Lemma EQ_MP {p q : Prop} (e : p = q) (h : p) : q.
-Proof. rewrite <- e. apply h. Qed.
-
-(****************************************************************************)
-(* Proof of some natural deduction rules. *)
-(****************************************************************************)
-
-Lemma or_intro1 {p:Prop} (h : p) (q:Prop) : p \/ q.
-Proof. exact (@or_introl p q h). Qed.
-
-Lemma or_intro2 (p:Prop) {q:Prop} (h : q) : p \/ q.
-Proof. exact (@or_intror p q h). Qed.
-
-Lemma or_elim {p q : Prop} (h : p \/ q) {r : Prop} (h1: p -> r) (h2: q -> r) : r.
-Proof. exact (@or_ind p q r h1 h2 h). Qed.
-
-Lemma ex_elim {a} {p : a -> Prop}
-  (h1 : exists x, p x) {r : Prop} (h2 : forall x : a, (p x) -> r) : r.
-Proof. exact (@ex_ind a p r h2 h1). Qed.
-
-(****************************************************************************)
-(* Coq axioms necessary to handle HOL-Light proofs. *)
-(****************************************************************************)
-
-Require Import Coq.Logic.ClassicalEpsilon.
-
-Definition ε : forall {A : Type'}, (type A -> Prop) -> type A :=
-  fun A P => epsilon (inhabits (el A)) P.
-
-Lemma ε_spec {A : Type'} {P : type A -> Prop} : (exists x, P x) -> P (ε P).
-Proof. intro h. unfold ε. apply epsilon_spec. exact h. Qed.
-
-Axiom fun_ext : forall {A B : Type} {f g : A -> B}, (forall x, (f x) = (g x)) -> f = g.
-
-Axiom prop_ext : forall {P Q : Prop}, (P -> Q) -> (Q -> P) -> P = Q.
-
-Require Import ClassicalFacts.
-
-Lemma prop_degen : forall P, P = True \/ P = False.
-Proof.
-  apply prop_ext_em_degen. unfold prop_extensionality. intros A B [AB BA].
-  apply prop_ext. exact AB. exact BA.
-  intro P. apply classic.
-Qed.
-
-Require Import PropExtensionalityFacts.
-
-Lemma is_True P : (P = True) = P.
-Proof.
-  apply prop_ext.
-  intro e. rewrite e. exact I.
-  apply PropExt_imp_ProvPropExt.
-  intros a b [ab ba]. apply prop_ext. apply ab. apply ba.
-Qed.
-
-Lemma is_False P : (P = False) = ~ P.
-Proof.
-  apply prop_ext; intro h. rewrite h. intro i. exact i.
-  apply prop_ext; intro i. apply h. apply i. apply False_rec. exact i.
-Qed.
-
-Lemma refl_is_True {A} (x:A) : (x = x) = True.
-Proof. rewrite is_True. reflexivity. Qed.
-
-Lemma sym {A} (x y : A) : (x = y) = (y = x).
-Proof. apply prop_ext; intro e; symmetry; exact e. Qed.
-
-Lemma True_and_True : (True /\ True) = True.
-Proof. rewrite is_True. tauto. Qed.
-
-Lemma not_forall_eq A (P : A -> Prop) : (~ forall x, P x) = exists x, ~ (P x).
-Proof.
-  apply prop_ext; intro h. apply not_all_ex_not. exact h.
-  apply ex_not_not_all. exact h.
-Qed.
-
-Lemma not_exists_eq A (P : A -> Prop) : (~ exists x, P x) = forall x, ~ (P x).
-Proof.
-  apply prop_ext; intro h. apply not_ex_all_not. exact h.
-  apply all_not_not_ex. exact h.
-Qed.
-
-Lemma ex2_eq A (P Q : A -> Prop) : (exists2 x, P x & Q x) = (exists x, P x /\ Q x).
-Proof.
-  apply prop_ext. intros [x h i]. exists x. auto. intros [x [h i]]. exists x; auto.
-Qed.
-
-Lemma not_conj_eq P Q : (~(P /\ Q)) = (~P \/ ~Q).
-Proof.
-  apply prop_ext; intro h.
-  case (classic P); intro i.
-  right. intro q. apply h. auto.
-  auto.
-  intros [p q]. destruct h as [h|h]; contradiction.
-Qed.
-
-Lemma not_disj_eq P Q : (~(P \/ Q)) = (~P /\ ~Q).
-Proof.
-  apply prop_ext; intro h.
-  split. intro p. apply h. left. exact p. intro q. apply h. right. exact q.
-  destruct h as [np nq]. intros [i|i]; auto.
-Qed.
-
-Lemma imp_eq_disj P Q : (P -> Q) = (~P \/ Q).
-Proof.
-  apply prop_ext; intro h.
-  case (classic P); intro i; auto.
-  intro p. destruct h as [h|h]. contradiction. exact h.
-Qed.
-
-Definition COND {A : Type'} := fun t : Prop => fun t1 : A => fun t2 : A => @ε A (fun x : A => ((t = True) -> x = t1) /\ ((t = False) -> x = t2)).
-
-Lemma COND_True (A : Type') (x y : A) : COND True x y = x.
-Proof.
-  unfold COND. match goal with [|- ε ?x = _] => set (Q := x) end.
-  assert (i : exists q, Q q). exists x. split; intro h.
-  reflexivity. apply False_rec. rewrite <- h. exact I.
-  generalize (ε_spec i). intros [h1 h2]. apply h1. reflexivity.
-Qed.
-
-Lemma COND_False (A : Type') (x y : A) : COND False x y = y.
-Proof.
-  unfold COND. match goal with [|- ε ?x = _] => set (Q := x) end.
-  assert (i : exists q, Q q). exists y. split; intro h. apply False_rec.
-  rewrite h. exact I. reflexivity.
-  generalize (ε_spec i). intros [h1 h2]. apply h2. reflexivity.
-Qed.
-
-Definition COND_dep (Q: Prop) (C: Type) (f1: Q -> C) (f2: ~Q -> C) : C :=
-  match excluded_middle_informative Q with
-  | left _ x => f1 x
-  | right _ x => f2 x
-  end.
-
-(****************************************************************************)
-(* Proof of HOL-Light axioms. *)
-(****************************************************************************)
-
-Lemma axiom_0 : forall {A B : Type'}, forall t : A -> B, (fun x : A => t x) = t.
-Proof. reflexivity. Qed.
-
-Lemma axiom_1 : forall {A : Type'}, forall P : A -> Prop, forall x : A, (P x) -> P (@ε A P).
-Proof.
-  intros A P x h. apply (epsilon_spec (inhabits (el A)) P (ex_intro P x h)).
-Qed.
-
-(*****************************************************************************)
-(* Alignment of subtypes. *)
-(*****************************************************************************)
-
-Require Import ProofIrrelevance.
-
-Section Subtype.
-
-  Variables (A : Type) (P : A -> Prop) (a : A) (h : P a).
-
-  Definition subtype := {| type := {x : A | P x}; el := exist P a h |}.
-
-  Definition dest : subtype -> A := fun x => proj1_sig x.
-
-  Definition mk : A -> subtype :=
-    fun x => COND_dep (P x) subtype (exist P x) (fun _ => exist P a h).
-
-  Lemma dest_mk_aux x : P x -> (dest (mk x) = x).
-  Proof.
-    intro hx. unfold mk, COND_dep. destruct excluded_middle_informative.
-    reflexivity. contradiction.
-  Qed.
-
-  Lemma dest_mk x : P x = (dest (mk x) = x).
-  Proof.
-    apply prop_ext. apply dest_mk_aux.
-    destruct (mk x) as [b i]. simpl. intro e. subst x. exact i.
-  Qed.
-
-  Lemma mk_dest x : mk (dest x) = x.
-  Proof.
-    unfold mk, COND_dep. destruct x as [b i]; simpl.
-    destruct excluded_middle_informative.
-    rewrite (proof_irrelevance _ p i). reflexivity.
-    contradiction.
-  Qed.
-
-  Lemma dest_inj x y : dest x = dest y -> x = y.
-  Proof.
-    intro e. destruct x as [x i]. destruct y as [y j]. simpl in e.
-    subst y. rewrite (proof_irrelevance _ i j). reflexivity.
-  Qed.
-
-  Lemma mk_inj x y : P x -> P y -> mk x = mk y -> x = y.
-  Proof.
-    intros hx hy. unfold mk, COND_dep.
-    destruct (excluded_middle_informative (P x));
-      destruct (excluded_middle_informative (P y)); intro e; inversion e.
-    reflexivity. contradiction. contradiction. contradiction.
-  Qed.
-
-End Subtype.
-
-Arguments subtype [A P a].
-Arguments mk [A P a].
-Arguments dest [A P a].
-Arguments dest_mk_aux [A P a].
-Arguments dest_mk [A P a].
-Arguments mk_dest [A P a].
-
-Canonical subtype.
-
-(*****************************************************************************)
-(* Alignment of quotients. *)
-(*****************************************************************************)
-
-Section Quotient.
-
-  Variables (A : Type') (R : A -> A -> Prop).
-
-  Definition is_eq_class X := exists a, X = R a.
-
-  Definition class_of x := R x.
-
-  Lemma is_eq_class_of x : is_eq_class (class_of x).
-  Proof. exists x. reflexivity. Qed.
-
-  Lemma non_empty : is_eq_class (class_of (el A)).
-  Proof. exists (el A). reflexivity. Qed.
-
-  Definition quotient := subtype non_empty.
-
-  Definition mk_quotient : (A -> Prop) -> quotient := mk non_empty.
-  Definition dest_quotient : quotient -> (A -> Prop) := dest non_empty.
-
-  Lemma mk_dest_quotient : forall x, mk_quotient (dest_quotient x) = x.
-  Proof. exact (mk_dest non_empty). Qed.
-
-  Lemma dest_mk_aux_quotient : forall x, is_eq_class x -> (dest_quotient (mk_quotient x) = x).
-  Proof. exact (dest_mk_aux non_empty). Qed.
-
-  Lemma dest_mk_quotient : forall x, is_eq_class x = (dest_quotient (mk_quotient x) = x).
-  Proof. exact (dest_mk non_empty). Qed.
-
-  Definition elt_of : quotient -> A := fun x => ε (dest_quotient x).
-
-  Variable R_refl : forall a, R a a.
-
-  Lemma eq_elt_of a : R a (ε (R a)).
-  Proof. apply ε_spec. exists a. apply R_refl. Qed.
-
-  Lemma dest_quotient_elt_of x : dest_quotient x (elt_of x).
-  Proof.
-    unfold elt_of, dest_quotient, dest. destruct x as [c [a h]]; simpl. subst c.
-    apply ε_spec. exists a. apply R_refl.
-  Qed.
-
-  Variable R_sym : forall x y, R x y -> R y x.
-  Variable R_trans : forall x y z, R x y -> R y z -> R x z.
-
-  Lemma dest_quotient_elim x y : dest_quotient x y -> R (elt_of x) y.
-  Proof.
-    unfold elt_of, dest_quotient, dest. destruct x as [c [a h]]; simpl. subst c.
-    intro h. apply R_trans with a. apply R_sym. apply eq_elt_of. exact h.
-  Qed.
-
-  Lemma eq_class_intro_elt (x y: quotient) : R (elt_of x) (elt_of y) -> x = y.
-  Proof.
-    destruct x as [c [x h]]. destruct y as [d [y i]]. unfold elt_of. simpl.
-    intro r. apply subset_eq_compat. subst c. subst d.
-    apply fun_ext; intro a. apply prop_ext; intro j.
-
-    apply R_trans with (ε (R y)). apply eq_elt_of.
-    apply R_trans with (ε (R x)). apply R_sym. apply r.
-    apply R_trans with x. apply R_sym. apply eq_elt_of. exact j.
-
-    apply R_trans with (ε (R x)). apply eq_elt_of.
-    apply R_trans with (ε (R y)). apply r.
-    apply R_trans with y. apply R_sym. apply eq_elt_of. exact j.
-  Qed.
-
-  Lemma eq_class_intro (x y: A) : R x y -> R x = R y.
-  Proof.
-    intro xy. apply fun_ext; intro a. apply prop_ext; intro h.
-    apply R_trans with x. apply R_sym. exact xy. exact h.
-    apply R_trans with y. exact xy. exact h.
-  Qed.
-
-  Lemma eq_class_elim (x y: A) : R x = R y -> R x y.
-  Proof.
-    intro h. generalize (ext_fun h y); intro hy.
-    assert (e : R y y = True). rewrite is_True. apply R_refl.
-    rewrite e, is_True in hy. exact hy.
-  Qed.
-
-  Lemma mk_quotient_elt_of x : mk_quotient (R (elt_of x)) = x.
-  Proof.
-    apply eq_class_intro_elt. set (a := elt_of x). unfold elt_of.
-    rewrite dest_mk_aux_quotient. apply R_sym. apply eq_elt_of.
-    exists a. reflexivity.
-  Qed.
-
-End Quotient.
-
-Arguments quotient [A].
-Arguments mk_quotient [A].
-Arguments dest_quotient [A].
-Arguments mk_dest_quotient [A].
-Arguments dest_mk_aux_quotient [A].
-Arguments dest_mk_quotient [A].
-Arguments is_eq_class [A].
-Arguments elt_of [A R].
-Arguments dest_quotient_elt_of [A R].
-
-(****************************************************************************)
-(* Alignment of connectives. *)
-(****************************************************************************)
-
-Lemma ex1_def : forall {A : Type'}, (@ex1 A) = (fun P : A -> Prop => (ex P) /\ (forall x : A, forall y : A, ((P x) /\ (P y)) -> x = y)).
-Proof.
-  intro A. unfold ex1. apply fun_ext; intro P. unfold unique. apply prop_ext.
-
-  intros [x [px u]]. split. apply (ex_intro P x px). intros a b [ha hb].
-  transitivity x. symmetry. apply u. exact ha. apply u. exact hb.
-
-  intros [[x px] u]. apply (ex_intro _ x). split. exact px. intros y py.
-  apply u. split. exact px. exact py.
-Qed.
-
-Lemma F_def : False = (forall p : Prop, p).
-Proof.
-  apply prop_ext. intros b p. apply (False_rec p b). intro h. exact (h False).
-Qed.
-
-Lemma not_def : not = (fun p : Prop => p -> False).
-Proof. reflexivity. Qed.
-
-Lemma or_def : or = (fun p : Prop => fun q : Prop => forall r : Prop, (p -> r) -> (q -> r) -> r).
-Proof.
-  apply fun_ext; intro p; apply fun_ext; intro q. apply prop_ext.
-  intros pq r pr qr. destruct pq. apply (pr H). apply (qr H).
-  intro h. apply h. intro hp. left. exact hp. intro hq. right. exact hq.
-Qed.
-
-Lemma ex_def : forall {A : Type'}, (@ex A) = (fun P : A -> Prop => forall q : Prop, (forall x : A, (P x) -> q) -> q).
-Proof.
-  intro A. apply fun_ext; intro p. apply prop_ext.
-  intros [x px] q pq. eapply pq. apply px.
-  intro h. apply h. intros x px. apply (ex_intro p x px).
-Qed.
-
-Lemma all_def : forall {A : Type'}, (@all A) = (fun P : A -> Prop => P = (fun x : A => True)).
-Proof.
-  intro A. apply fun_ext; intro p. apply prop_ext.
-  intro h. apply fun_ext; intro x. apply prop_ext.
-  intros _. exact I. intros _. exact (h x).
-  intros e x. rewrite e. exact I.
-Qed.
-
-Lemma imp_def : imp = (fun p : Prop => fun q : Prop => (p /\ q) = p).
-Proof.
-  apply fun_ext; intro p. apply fun_ext; intro q. apply prop_ext.
-  intro pq. apply prop_ext. intros [hp _]. exact hp. intro hp.
-  split. exact hp. apply pq. exact hp.
-  intro e. rewrite <- e. intros [_ hq]. exact hq.
-Qed.
-
-Lemma and_def : and = (fun p : Prop => fun q : Prop => (fun f : Prop -> Prop -> Prop => f p q) = (fun f : Prop -> Prop -> Prop => f True True)).
-Proof.
-  apply fun_ext; intro p. apply fun_ext; intro q. apply prop_ext.
-
-  intros [hp hq]. apply fun_ext; intro f.
-  case (prop_degen p); intro e; subst p.
-  case (prop_degen q); intro e; subst q.
-  reflexivity.
-  exfalso. exact hq.
-  exfalso. exact hp.
-
-  intro e. generalize (ext_fun e); clear e; intro e. split.
-  rewrite (e (fun p _ => p)). exact I.
-  rewrite (e (fun _ q => q)). exact I.
-Qed.
-
-Lemma T_def : True = ((fun p : Prop => p) = (fun p : Prop => p)).
-Proof. apply prop_ext. reflexivity. intros _; exact I. Qed.
-
-(****************************************************************************)
-(* Alignment of the unit type. *)
-(****************************************************************************)
-
-Definition unit' := {| type := unit; el := tt |}.
-Canonical unit'.
-
-Definition one_ABS : Prop -> unit := fun _ => tt.
-
-Definition one_REP : unit -> Prop := fun _ => True.
-
-Lemma axiom_2 : forall (a : unit), (one_ABS (one_REP a)) = a.
-Proof. intro a. destruct a. reflexivity. Qed.
-
-Lemma axiom_3 : forall (r : Prop), ((fun b : Prop => b) r) = ((one_REP (one_ABS r)) = r).
-Proof. intro r. compute. rewrite (sym True r), is_True. reflexivity. Qed.
-
-Lemma one_def : tt = ε one_REP.
-Proof. generalize (ε one_REP). destruct t. reflexivity. Qed.
-
-(****************************************************************************)
-(* Alignment of the product type constructor. *)
-(****************************************************************************)
-
-Definition prod' (a b : Type') := {| type := a * b; el := pair (el a) (el b) |}.
-Canonical prod'.
-
-Definition mk_pair {A B : Type'} :=
-  fun x : A => fun y : B => fun a : A => fun b : B => (a = x) /\ (b = y).
-
-Lemma mk_pair_inj (A B : Type') (x x' : A) (y y' : B) :
-  mk_pair x y = mk_pair x' y' -> x = x' /\ y = y'.
-Proof.
-  intro e; generalize (ext_fun e); clear e; intro e.
-  generalize (ext_fun (e x)); clear e; intro e.
-  generalize (e y); clear e. unfold mk_pair.
-  rewrite refl_is_True, refl_is_True, True_and_True, sym, is_True.
-  intro h; exact h.
-Qed.
-
-Definition ABS_prod : forall {A B : Type'}, (A -> B -> Prop) -> prod A B :=
-  fun A B f => ε (fun p => f = mk_pair (fst p) (snd p)).
-
-Lemma ABS_prod_mk_pair (A B : Type') (x : A) (y : B) :
-  ABS_prod (mk_pair x y) = (x,y).
-Proof.
-  unfold ABS_prod.
-  match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end.
-  rewrite (surjective_pairing q).
-  assert (i : exists q, Q q). exists (x,y). reflexivity.
-  generalize (ε_spec i); fold q; unfold Q; intro h.
-  apply mk_pair_inj in h. destruct h as [h1 h2]. rewrite h1, h2. reflexivity.
-Qed.
-
-Lemma ABS_prod_mk_pair_eta (A B : Type') (x : A) (y : B) :
-  ABS_prod (fun a b => mk_pair x y a b) = (x,y).
-Proof.
-  unfold ABS_prod.
-  match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end.
-  rewrite (surjective_pairing q).
-  assert (i : exists q, Q q). exists (x,y). reflexivity.
-  generalize (ε_spec i); fold q; unfold Q; intro h.
-  apply mk_pair_inj in h. destruct h as [h1 h2]. rewrite h1, h2. reflexivity.
-Qed.
-
-Definition REP_prod : forall {A B : Type'}, (prod A B) -> A -> B -> Prop :=
-  fun A B p a b => mk_pair (fst p) (snd p) a b.
-
-Lemma pair_def {A B : Type'} : (@pair A B) = (fun x : A => fun y : B => @ABS_prod A B (@mk_pair A B x y)).
-Proof.
-  apply fun_ext; intro x; apply fun_ext; intro y. symmetry.
-  apply ABS_prod_mk_pair.
-Qed.
-
-Lemma FST_def {A B : Type'} : (@fst A B) = (fun p : prod A B => @ε A (fun x : A => exists y : B, p = (@pair A B x y))).
-Proof.
-  apply fun_ext; intros [x y]. simpl.
-  match goal with [|- _ = ε ?x] => set (Q := x); set (q := ε Q) end.
-  assert (i : exists x, Q x). exists x. exists y. reflexivity.
-  generalize (ε_spec i); fold q; intros [x' h']. inversion h'. reflexivity.
-Qed.
-
-Lemma SND_def {A B : Type'} : (@snd A B) = (fun p : prod A B => @ε B (fun y : B => exists x : A, p = (@pair A B x y))).
-Proof.
-  apply fun_ext; intros [x y]. simpl.
-  match goal with [|- _ = ε ?x] => set (Q := x); set (q := ε Q) end.
-  assert (i : exists x, Q x). exists y. exists x. reflexivity.
-  generalize (ε_spec i); fold q; intros [x' h]. inversion h. reflexivity.
-Qed.
-
-Lemma axiom_4 : forall {A B : Type'} (a : prod A B), (@ABS_prod A B (@REP_prod A B a)) = a.
-Proof. intros A B [a b]. apply ABS_prod_mk_pair_eta. Qed.
-
-Lemma axiom_5 : forall {A B : Type'} (r : A -> B -> Prop), ((fun x : A -> B -> Prop => exists a : A, exists b : B, x = (@mk_pair A B a b)) r) = ((@REP_prod A B (@ABS_prod A B r)) = r).
-Proof.
-  intros A B f. simpl. apply prop_ext.
-  intros [a [b e]]. subst. rewrite ABS_prod_mk_pair. reflexivity.
-  generalize (ABS_prod f); intros [a b] e. subst. exists a. exists b. reflexivity.
-Qed.
-
-(****************************************************************************)
-(* Alignment of the infinite type ind. *)
-(****************************************************************************)
-
-Definition nat' := {| type := nat; el := 0 |}.
-Canonical nat'.
-
-Definition ind : Type' := nat'.
-
-Definition ONE_ONE {A B : Type'} := fun _2064 : A -> B => forall x1 : A, forall x2 : A, ((_2064 x1) = (_2064 x2)) -> x1 = x2.
-
-Definition ONTO {A B : Type'} := fun _2069 : A -> B => forall y : B, exists x : A, y = (_2069 x).
-
-Lemma axiom_6 : exists f : ind -> ind, (@ONE_ONE ind ind f) /\ (~ (@ONTO ind ind f)).
-Proof.
-  exists S. split. exact eq_add_S. intro h. generalize (h 0). intros [x hx].
-  discriminate.
-Qed.
-
-Definition IND_SUC_pred := fun f : ind -> ind => exists z : ind, (forall x1 : ind, forall x2 : ind, ((f x1) = (f x2)) = (x1 = x2)) /\ (forall x : ind, ~ ((f x) = z)).
-
-Definition IND_SUC := ε IND_SUC_pred.
-
-Lemma IND_SUC_ex : exists f, IND_SUC_pred f.
-Proof.
-  destruct axiom_6 as [f [h1 h2]]. exists f.
-  unfold ONTO in h2. rewrite not_forall_eq in h2. destruct h2 as [z h2]. exists z.
-  split.
-  intros x y. apply prop_ext. apply h1. intro e. rewrite e. reflexivity.
-  rewrite not_exists_eq in h2. intros x e. apply (h2 x). symmetry. exact e.
-Qed.
-
-Lemma IND_SUC_prop : IND_SUC_pred IND_SUC.
-Proof. unfold IND_SUC. apply ε_spec. apply IND_SUC_ex. Qed.
-
-Lemma IND_SUC_inj : ONE_ONE IND_SUC.
-Proof.
-  generalize IND_SUC_prop. intros [z [h1 h2]]. intros x y e. rewrite <- h1.
-  exact e.
-Qed.
-
-Definition IND_0_pred := fun z : ind => (forall x1 : ind, forall x2 : ind, ((IND_SUC x1) = (IND_SUC x2)) = (x1 = x2)) /\ (forall x : ind, ~ ((IND_SUC x) = z)).
-
-Definition IND_0 := ε IND_0_pred.
-
-Lemma IND_0_ex : exists z, IND_0_pred z.
-Proof.
-  generalize IND_SUC_prop. intros [z [h1 h2]]. exists z. split. exact h1. exact h2.
-Qed.
-
-Lemma IND_0_prop : IND_0_pred IND_0.
-Proof. unfold IND_0. apply ε_spec. apply IND_0_ex. Qed.
-
-Lemma IND_SUC_neq_0 i : IND_SUC i <> IND_0.
-Proof. generalize IND_0_prop. intros [h1 h2]. apply h2. Qed.
-
-(****************************************************************************)
-(* Properties of NUM_REP. *)
-(****************************************************************************)
-
-Definition NUM_REP := fun a : ind => forall NUM_REP' : ind -> Prop, (forall a' : ind, ((a' = IND_0) \/ (exists i : ind, (a' = (IND_SUC i)) /\ (NUM_REP' i))) -> NUM_REP' a') -> NUM_REP' a.
-
-Definition NUM_REP' := fun a : ind => forall P : ind -> Prop, (P IND_0 /\ forall i, P i -> P (IND_SUC i)) -> P a.
-
-Lemma NUM_REP_eq : NUM_REP = NUM_REP'.
-Proof.
-  apply fun_ext; intro a. apply prop_ext; intros h P.
-  intros [p0 ps]. apply h. intros a' [i|i].
-    subst a'. exact p0.
-    destruct i as [b [e i]]. subst a'. apply ps. exact i.
-  intro i. apply h. split.
-    apply i. left. reflexivity.
-    intros b pb. apply i. right. exists b. split. reflexivity. exact pb.
-Qed.
-
-Lemma NUM_REP_0 : NUM_REP IND_0.
-Proof. rewrite NUM_REP_eq. intros P [h _]. exact h. Qed.
-
-Lemma NUM_REP_S i : NUM_REP i -> NUM_REP (IND_SUC i).
-Proof.
-  rewrite NUM_REP_eq. intros hi P [h0 hS]. apply hS. apply hi.
-  split. exact h0. exact hS.
-Qed.
-
-Inductive NUM_REP_ID : ind -> Prop :=
-  | NUM_REP_ID_0 : NUM_REP_ID IND_0
-  | NUM_REP_ID_S i : NUM_REP_ID i -> NUM_REP_ID (IND_SUC i).
-
-Lemma NUM_REP_eq_ID : NUM_REP = NUM_REP_ID.
-Proof.
-  apply fun_ext; intro i. apply prop_ext.
-  rewrite NUM_REP_eq. intro h. apply h. split.
-    apply NUM_REP_ID_0.
-    intros j hj. apply NUM_REP_ID_S. exact hj.
-  induction 1. apply NUM_REP_0. apply NUM_REP_S. assumption.
-Qed.
diff --git a/erasing.lp b/mappings.lp
similarity index 100%
rename from erasing.lp
rename to mappings.lp
diff --git a/mappings.v b/mappings.v
index b02f76f..a1e8ded 100644
--- a/mappings.v
+++ b/mappings.v
@@ -1,4 +1,628 @@
-Require Import HOLLight_Real_With_N.logic BinNat Lia Coq.Logic.ClassicalEpsilon.
+(****************************************************************************)
+(* Coq theory for encoding HOL-Light proofs. *)
+(****************************************************************************)
+
+Lemma ext_fun {A B} {f g : A -> B} : f = g -> forall x, f x = g x.
+Proof. intros fg x. rewrite fg. reflexivity. Qed.
+
+Lemma eq_false_negb_true b : b = false -> negb b = true.
+Proof. intro e. subst. reflexivity. Qed.
+
+(****************************************************************************)
+(* Type of non-empty types, used to interpret HOL-Light types types. *)
+(****************************************************************************)
+
+Record Type' := { type :> Type; el : type }.
+
+Definition bool' := {| type := bool; el := true |}.
+Canonical bool'.
+
+Definition Prop' : Type' := {| type := Prop; el := True |}.
+Canonical Prop'.
+
+Definition arr a (b : Type') := {| type := a -> b; el := fun _ => el b |}.
+Canonical arr.
+
+(****************************************************************************)
+(* Curryfied versions of some Coq connectives. *)
+(****************************************************************************)
+
+Definition imp (p q : Prop) : Prop := p -> q.
+
+Definition ex1 : forall {A : Type'}, (A -> Prop) -> Prop := fun A P => exists! x, P x.
+
+(****************************************************************************)
+(* Proof of some HOL-Light rules. *)
+(****************************************************************************)
+
+Lemma MK_COMB {a b : Type} {s t : a -> b} {u v : a} (h1 : s = t) (h2 : u = v)
+  : (s u) = (t v).
+Proof. rewrite h1, h2. reflexivity. Qed.
+
+Lemma EQ_MP {p q : Prop} (e : p = q) (h : p) : q.
+Proof. rewrite <- e. apply h. Qed.
+
+(****************************************************************************)
+(* Proof of some natural deduction rules. *)
+(****************************************************************************)
+
+Lemma or_intro1 {p:Prop} (h : p) (q:Prop) : p \/ q.
+Proof. exact (@or_introl p q h). Qed.
+
+Lemma or_intro2 (p:Prop) {q:Prop} (h : q) : p \/ q.
+Proof. exact (@or_intror p q h). Qed.
+
+Lemma or_elim {p q : Prop} (h : p \/ q) {r : Prop} (h1: p -> r) (h2: q -> r) : r.
+Proof. exact (@or_ind p q r h1 h2 h). Qed.
+
+Lemma ex_elim {a} {p : a -> Prop}
+  (h1 : exists x, p x) {r : Prop} (h2 : forall x : a, (p x) -> r) : r.
+Proof. exact (@ex_ind a p r h2 h1). Qed.
+
+(****************************************************************************)
+(* Coq axioms necessary to handle HOL-Light proofs. *)
+(****************************************************************************)
+
+Require Import Coq.Logic.ClassicalEpsilon.
+
+Definition ε : forall {A : Type'}, (type A -> Prop) -> type A :=
+  fun A P => epsilon (inhabits (el A)) P.
+
+Lemma ε_spec {A : Type'} {P : type A -> Prop} : (exists x, P x) -> P (ε P).
+Proof. intro h. unfold ε. apply epsilon_spec. exact h. Qed.
+
+Axiom fun_ext : forall {A B : Type} {f g : A -> B}, (forall x, (f x) = (g x)) -> f = g.
+
+Axiom prop_ext : forall {P Q : Prop}, (P -> Q) -> (Q -> P) -> P = Q.
+
+Require Import ClassicalFacts.
+
+Lemma prop_degen : forall P, P = True \/ P = False.
+Proof.
+  apply prop_ext_em_degen. unfold prop_extensionality. intros A B [AB BA].
+  apply prop_ext. exact AB. exact BA.
+  intro P. apply classic.
+Qed.
+
+Require Import PropExtensionalityFacts.
+
+Lemma is_True P : (P = True) = P.
+Proof.
+  apply prop_ext.
+  intro e. rewrite e. exact I.
+  apply PropExt_imp_ProvPropExt.
+  intros a b [ab ba]. apply prop_ext. apply ab. apply ba.
+Qed.
+
+Lemma is_False P : (P = False) = ~ P.
+Proof.
+  apply prop_ext; intro h. rewrite h. intro i. exact i.
+  apply prop_ext; intro i. apply h. apply i. apply False_rec. exact i.
+Qed.
+
+Lemma refl_is_True {A} (x:A) : (x = x) = True.
+Proof. rewrite is_True. reflexivity. Qed.
+
+Lemma sym {A} (x y : A) : (x = y) = (y = x).
+Proof. apply prop_ext; intro e; symmetry; exact e. Qed.
+
+Lemma True_and_True : (True /\ True) = True.
+Proof. rewrite is_True. tauto. Qed.
+
+Lemma not_forall_eq A (P : A -> Prop) : (~ forall x, P x) = exists x, ~ (P x).
+Proof.
+  apply prop_ext; intro h. apply not_all_ex_not. exact h.
+  apply ex_not_not_all. exact h.
+Qed.
+
+Lemma not_exists_eq A (P : A -> Prop) : (~ exists x, P x) = forall x, ~ (P x).
+Proof.
+  apply prop_ext; intro h. apply not_ex_all_not. exact h.
+  apply all_not_not_ex. exact h.
+Qed.
+
+Lemma ex2_eq A (P Q : A -> Prop) : (exists2 x, P x & Q x) = (exists x, P x /\ Q x).
+Proof.
+  apply prop_ext. intros [x h i]. exists x. auto. intros [x [h i]]. exists x; auto.
+Qed.
+
+Lemma not_conj_eq P Q : (~(P /\ Q)) = (~P \/ ~Q).
+Proof.
+  apply prop_ext; intro h.
+  case (classic P); intro i.
+  right. intro q. apply h. auto.
+  auto.
+  intros [p q]. destruct h as [h|h]; contradiction.
+Qed.
+
+Lemma not_disj_eq P Q : (~(P \/ Q)) = (~P /\ ~Q).
+Proof.
+  apply prop_ext; intro h.
+  split. intro p. apply h. left. exact p. intro q. apply h. right. exact q.
+  destruct h as [np nq]. intros [i|i]; auto.
+Qed.
+
+Lemma imp_eq_disj P Q : (P -> Q) = (~P \/ Q).
+Proof.
+  apply prop_ext; intro h.
+  case (classic P); intro i; auto.
+  intro p. destruct h as [h|h]. contradiction. exact h.
+Qed.
+
+Definition COND {A : Type'} := fun t : Prop => fun t1 : A => fun t2 : A => @ε A (fun x : A => ((t = True) -> x = t1) /\ ((t = False) -> x = t2)).
+
+Lemma COND_True (A : Type') (x y : A) : COND True x y = x.
+Proof.
+  unfold COND. match goal with [|- ε ?x = _] => set (Q := x) end.
+  assert (i : exists q, Q q). exists x. split; intro h.
+  reflexivity. apply False_rec. rewrite <- h. exact I.
+  generalize (ε_spec i). intros [h1 h2]. apply h1. reflexivity.
+Qed.
+
+Lemma COND_False (A : Type') (x y : A) : COND False x y = y.
+Proof.
+  unfold COND. match goal with [|- ε ?x = _] => set (Q := x) end.
+  assert (i : exists q, Q q). exists y. split; intro h. apply False_rec.
+  rewrite h. exact I. reflexivity.
+  generalize (ε_spec i). intros [h1 h2]. apply h2. reflexivity.
+Qed.
+
+Definition COND_dep (Q: Prop) (C: Type) (f1: Q -> C) (f2: ~Q -> C) : C :=
+  match excluded_middle_informative Q with
+  | left _ x => f1 x
+  | right _ x => f2 x
+  end.
+
+(****************************************************************************)
+(* Proof of HOL-Light axioms. *)
+(****************************************************************************)
+
+Lemma axiom_0 : forall {A B : Type'}, forall t : A -> B, (fun x : A => t x) = t.
+Proof. reflexivity. Qed.
+
+Lemma axiom_1 : forall {A : Type'}, forall P : A -> Prop, forall x : A, (P x) -> P (@ε A P).
+Proof.
+  intros A P x h. apply (epsilon_spec (inhabits (el A)) P (ex_intro P x h)).
+Qed.
+
+(*****************************************************************************)
+(* Alignment of subtypes. *)
+(*****************************************************************************)
+
+Require Import ProofIrrelevance.
+
+Section Subtype.
+
+  Variables (A : Type) (P : A -> Prop) (a : A) (h : P a).
+
+  Definition subtype := {| type := {x : A | P x}; el := exist P a h |}.
+
+  Definition dest : subtype -> A := fun x => proj1_sig x.
+
+  Definition mk : A -> subtype :=
+    fun x => COND_dep (P x) subtype (exist P x) (fun _ => exist P a h).
+
+  Lemma dest_mk_aux x : P x -> (dest (mk x) = x).
+  Proof.
+    intro hx. unfold mk, COND_dep. destruct excluded_middle_informative.
+    reflexivity. contradiction.
+  Qed.
+
+  Lemma dest_mk x : P x = (dest (mk x) = x).
+  Proof.
+    apply prop_ext. apply dest_mk_aux.
+    destruct (mk x) as [b i]. simpl. intro e. subst x. exact i.
+  Qed.
+
+  Lemma mk_dest x : mk (dest x) = x.
+  Proof.
+    unfold mk, COND_dep. destruct x as [b i]; simpl.
+    destruct excluded_middle_informative.
+    rewrite (proof_irrelevance _ p i). reflexivity.
+    contradiction.
+  Qed.
+
+  Lemma dest_inj x y : dest x = dest y -> x = y.
+  Proof.
+    intro e. destruct x as [x i]. destruct y as [y j]. simpl in e.
+    subst y. rewrite (proof_irrelevance _ i j). reflexivity.
+  Qed.
+
+  Lemma mk_inj x y : P x -> P y -> mk x = mk y -> x = y.
+  Proof.
+    intros hx hy. unfold mk, COND_dep.
+    destruct (excluded_middle_informative (P x));
+      destruct (excluded_middle_informative (P y)); intro e; inversion e.
+    reflexivity. contradiction. contradiction. contradiction.
+  Qed.
+
+End Subtype.
+
+Arguments subtype [A P a].
+Arguments mk [A P a].
+Arguments dest [A P a].
+Arguments dest_mk_aux [A P a].
+Arguments dest_mk [A P a].
+Arguments mk_dest [A P a].
+
+Canonical subtype.
+
+(*****************************************************************************)
+(* Alignment of quotients. *)
+(*****************************************************************************)
+
+Section Quotient.
+
+  Variables (A : Type') (R : A -> A -> Prop).
+
+  Definition is_eq_class X := exists a, X = R a.
+
+  Definition class_of x := R x.
+
+  Lemma is_eq_class_of x : is_eq_class (class_of x).
+  Proof. exists x. reflexivity. Qed.
+
+  Lemma non_empty : is_eq_class (class_of (el A)).
+  Proof. exists (el A). reflexivity. Qed.
+
+  Definition quotient := subtype non_empty.
+
+  Definition mk_quotient : (A -> Prop) -> quotient := mk non_empty.
+  Definition dest_quotient : quotient -> (A -> Prop) := dest non_empty.
+
+  Lemma mk_dest_quotient : forall x, mk_quotient (dest_quotient x) = x.
+  Proof. exact (mk_dest non_empty). Qed.
+
+  Lemma dest_mk_aux_quotient : forall x, is_eq_class x -> (dest_quotient (mk_quotient x) = x).
+  Proof. exact (dest_mk_aux non_empty). Qed.
+
+  Lemma dest_mk_quotient : forall x, is_eq_class x = (dest_quotient (mk_quotient x) = x).
+  Proof. exact (dest_mk non_empty). Qed.
+
+  Definition elt_of : quotient -> A := fun x => ε (dest_quotient x).
+
+  Variable R_refl : forall a, R a a.
+
+  Lemma eq_elt_of a : R a (ε (R a)).
+  Proof. apply ε_spec. exists a. apply R_refl. Qed.
+
+  Lemma dest_quotient_elt_of x : dest_quotient x (elt_of x).
+  Proof.
+    unfold elt_of, dest_quotient, dest. destruct x as [c [a h]]; simpl. subst c.
+    apply ε_spec. exists a. apply R_refl.
+  Qed.
+
+  Variable R_sym : forall x y, R x y -> R y x.
+  Variable R_trans : forall x y z, R x y -> R y z -> R x z.
+
+  Lemma dest_quotient_elim x y : dest_quotient x y -> R (elt_of x) y.
+  Proof.
+    unfold elt_of, dest_quotient, dest. destruct x as [c [a h]]; simpl. subst c.
+    intro h. apply R_trans with a. apply R_sym. apply eq_elt_of. exact h.
+  Qed.
+
+  Lemma eq_class_intro_elt (x y: quotient) : R (elt_of x) (elt_of y) -> x = y.
+  Proof.
+    destruct x as [c [x h]]. destruct y as [d [y i]]. unfold elt_of. simpl.
+    intro r. apply subset_eq_compat. subst c. subst d.
+    apply fun_ext; intro a. apply prop_ext; intro j.
+
+    apply R_trans with (ε (R y)). apply eq_elt_of.
+    apply R_trans with (ε (R x)). apply R_sym. apply r.
+    apply R_trans with x. apply R_sym. apply eq_elt_of. exact j.
+
+    apply R_trans with (ε (R x)). apply eq_elt_of.
+    apply R_trans with (ε (R y)). apply r.
+    apply R_trans with y. apply R_sym. apply eq_elt_of. exact j.
+  Qed.
+
+  Lemma eq_class_intro (x y: A) : R x y -> R x = R y.
+  Proof.
+    intro xy. apply fun_ext; intro a. apply prop_ext; intro h.
+    apply R_trans with x. apply R_sym. exact xy. exact h.
+    apply R_trans with y. exact xy. exact h.
+  Qed.
+
+  Lemma eq_class_elim (x y: A) : R x = R y -> R x y.
+  Proof.
+    intro h. generalize (ext_fun h y); intro hy.
+    assert (e : R y y = True). rewrite is_True. apply R_refl.
+    rewrite e, is_True in hy. exact hy.
+  Qed.
+
+  Lemma mk_quotient_elt_of x : mk_quotient (R (elt_of x)) = x.
+  Proof.
+    apply eq_class_intro_elt. set (a := elt_of x). unfold elt_of.
+    rewrite dest_mk_aux_quotient. apply R_sym. apply eq_elt_of.
+    exists a. reflexivity.
+  Qed.
+
+End Quotient.
+
+Arguments quotient [A].
+Arguments mk_quotient [A].
+Arguments dest_quotient [A].
+Arguments mk_dest_quotient [A].
+Arguments dest_mk_aux_quotient [A].
+Arguments dest_mk_quotient [A].
+Arguments is_eq_class [A].
+Arguments elt_of [A R].
+Arguments dest_quotient_elt_of [A R].
+
+(****************************************************************************)
+(* Alignment of connectives. *)
+(****************************************************************************)
+
+Lemma ex1_def : forall {A : Type'}, (@ex1 A) = (fun P : A -> Prop => (ex P) /\ (forall x : A, forall y : A, ((P x) /\ (P y)) -> x = y)).
+Proof.
+  intro A. unfold ex1. apply fun_ext; intro P. unfold unique. apply prop_ext.
+
+  intros [x [px u]]. split. apply (ex_intro P x px). intros a b [ha hb].
+  transitivity x. symmetry. apply u. exact ha. apply u. exact hb.
+
+  intros [[x px] u]. apply (ex_intro _ x). split. exact px. intros y py.
+  apply u. split. exact px. exact py.
+Qed.
+
+Lemma F_def : False = (forall p : Prop, p).
+Proof.
+  apply prop_ext. intros b p. apply (False_rec p b). intro h. exact (h False).
+Qed.
+
+Lemma not_def : not = (fun p : Prop => p -> False).
+Proof. reflexivity. Qed.
+
+Lemma or_def : or = (fun p : Prop => fun q : Prop => forall r : Prop, (p -> r) -> (q -> r) -> r).
+Proof.
+  apply fun_ext; intro p; apply fun_ext; intro q. apply prop_ext.
+  intros pq r pr qr. destruct pq. apply (pr H). apply (qr H).
+  intro h. apply h. intro hp. left. exact hp. intro hq. right. exact hq.
+Qed.
+
+Lemma ex_def : forall {A : Type'}, (@ex A) = (fun P : A -> Prop => forall q : Prop, (forall x : A, (P x) -> q) -> q).
+Proof.
+  intro A. apply fun_ext; intro p. apply prop_ext.
+  intros [x px] q pq. eapply pq. apply px.
+  intro h. apply h. intros x px. apply (ex_intro p x px).
+Qed.
+
+Lemma all_def : forall {A : Type'}, (@all A) = (fun P : A -> Prop => P = (fun x : A => True)).
+Proof.
+  intro A. apply fun_ext; intro p. apply prop_ext.
+  intro h. apply fun_ext; intro x. apply prop_ext.
+  intros _. exact I. intros _. exact (h x).
+  intros e x. rewrite e. exact I.
+Qed.
+
+Lemma imp_def : imp = (fun p : Prop => fun q : Prop => (p /\ q) = p).
+Proof.
+  apply fun_ext; intro p. apply fun_ext; intro q. apply prop_ext.
+  intro pq. apply prop_ext. intros [hp _]. exact hp. intro hp.
+  split. exact hp. apply pq. exact hp.
+  intro e. rewrite <- e. intros [_ hq]. exact hq.
+Qed.
+
+Lemma and_def : and = (fun p : Prop => fun q : Prop => (fun f : Prop -> Prop -> Prop => f p q) = (fun f : Prop -> Prop -> Prop => f True True)).
+Proof.
+  apply fun_ext; intro p. apply fun_ext; intro q. apply prop_ext.
+
+  intros [hp hq]. apply fun_ext; intro f.
+  case (prop_degen p); intro e; subst p.
+  case (prop_degen q); intro e; subst q.
+  reflexivity.
+  exfalso. exact hq.
+  exfalso. exact hp.
+
+  intro e. generalize (ext_fun e); clear e; intro e. split.
+  rewrite (e (fun p _ => p)). exact I.
+  rewrite (e (fun _ q => q)). exact I.
+Qed.
+
+Lemma T_def : True = ((fun p : Prop => p) = (fun p : Prop => p)).
+Proof. apply prop_ext. reflexivity. intros _; exact I. Qed.
+
+(****************************************************************************)
+(* Alignment of the unit type. *)
+(****************************************************************************)
+
+Definition unit' := {| type := unit; el := tt |}.
+Canonical unit'.
+
+Definition one_ABS : Prop -> unit := fun _ => tt.
+
+Definition one_REP : unit -> Prop := fun _ => True.
+
+Lemma axiom_2 : forall (a : unit), (one_ABS (one_REP a)) = a.
+Proof. intro a. destruct a. reflexivity. Qed.
+
+Lemma axiom_3 : forall (r : Prop), ((fun b : Prop => b) r) = ((one_REP (one_ABS r)) = r).
+Proof. intro r. compute. rewrite (sym True r), is_True. reflexivity. Qed.
+
+Lemma one_def : tt = ε one_REP.
+Proof. generalize (ε one_REP). destruct t. reflexivity. Qed.
+
+(****************************************************************************)
+(* Alignment of the product type constructor. *)
+(****************************************************************************)
+
+Definition prod' (a b : Type') := {| type := a * b; el := pair (el a) (el b) |}.
+Canonical prod'.
+
+Definition mk_pair {A B : Type'} :=
+  fun x : A => fun y : B => fun a : A => fun b : B => (a = x) /\ (b = y).
+
+Lemma mk_pair_inj (A B : Type') (x x' : A) (y y' : B) :
+  mk_pair x y = mk_pair x' y' -> x = x' /\ y = y'.
+Proof.
+  intro e; generalize (ext_fun e); clear e; intro e.
+  generalize (ext_fun (e x)); clear e; intro e.
+  generalize (e y); clear e. unfold mk_pair.
+  rewrite refl_is_True, refl_is_True, True_and_True, sym, is_True.
+  intro h; exact h.
+Qed.
+
+Definition ABS_prod : forall {A B : Type'}, (A -> B -> Prop) -> prod A B :=
+  fun A B f => ε (fun p => f = mk_pair (fst p) (snd p)).
+
+Lemma ABS_prod_mk_pair (A B : Type') (x : A) (y : B) :
+  ABS_prod (mk_pair x y) = (x,y).
+Proof.
+  unfold ABS_prod.
+  match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end.
+  rewrite (surjective_pairing q).
+  assert (i : exists q, Q q). exists (x,y). reflexivity.
+  generalize (ε_spec i); fold q; unfold Q; intro h.
+  apply mk_pair_inj in h. destruct h as [h1 h2]. rewrite h1, h2. reflexivity.
+Qed.
+
+Lemma ABS_prod_mk_pair_eta (A B : Type') (x : A) (y : B) :
+  ABS_prod (fun a b => mk_pair x y a b) = (x,y).
+Proof.
+  unfold ABS_prod.
+  match goal with [|- ε ?x = _] => set (Q := x); set (q := ε Q) end.
+  rewrite (surjective_pairing q).
+  assert (i : exists q, Q q). exists (x,y). reflexivity.
+  generalize (ε_spec i); fold q; unfold Q; intro h.
+  apply mk_pair_inj in h. destruct h as [h1 h2]. rewrite h1, h2. reflexivity.
+Qed.
+
+Definition REP_prod : forall {A B : Type'}, (prod A B) -> A -> B -> Prop :=
+  fun A B p a b => mk_pair (fst p) (snd p) a b.
+
+Lemma pair_def {A B : Type'} : (@pair A B) = (fun x : A => fun y : B => @ABS_prod A B (@mk_pair A B x y)).
+Proof.
+  apply fun_ext; intro x; apply fun_ext; intro y. symmetry.
+  apply ABS_prod_mk_pair.
+Qed.
+
+Lemma FST_def {A B : Type'} : (@fst A B) = (fun p : prod A B => @ε A (fun x : A => exists y : B, p = (@pair A B x y))).
+Proof.
+  apply fun_ext; intros [x y]. simpl.
+  match goal with [|- _ = ε ?x] => set (Q := x); set (q := ε Q) end.
+  assert (i : exists x, Q x). exists x. exists y. reflexivity.
+  generalize (ε_spec i); fold q; intros [x' h']. inversion h'. reflexivity.
+Qed.
+
+Lemma SND_def {A B : Type'} : (@snd A B) = (fun p : prod A B => @ε B (fun y : B => exists x : A, p = (@pair A B x y))).
+Proof.
+  apply fun_ext; intros [x y]. simpl.
+  match goal with [|- _ = ε ?x] => set (Q := x); set (q := ε Q) end.
+  assert (i : exists x, Q x). exists y. exists x. reflexivity.
+  generalize (ε_spec i); fold q; intros [x' h]. inversion h. reflexivity.
+Qed.
+
+Lemma axiom_4 : forall {A B : Type'} (a : prod A B), (@ABS_prod A B (@REP_prod A B a)) = a.
+Proof. intros A B [a b]. apply ABS_prod_mk_pair_eta. Qed.
+
+Lemma axiom_5 : forall {A B : Type'} (r : A -> B -> Prop), ((fun x : A -> B -> Prop => exists a : A, exists b : B, x = (@mk_pair A B a b)) r) = ((@REP_prod A B (@ABS_prod A B r)) = r).
+Proof.
+  intros A B f. simpl. apply prop_ext.
+  intros [a [b e]]. subst. rewrite ABS_prod_mk_pair. reflexivity.
+  generalize (ABS_prod f); intros [a b] e. subst. exists a. exists b. reflexivity.
+Qed.
+
+(****************************************************************************)
+(* Alignment of the infinite type ind. *)
+(****************************************************************************)
+
+Definition nat' := {| type := nat; el := 0 |}.
+Canonical nat'.
+
+Definition ind : Type' := nat'.
+
+Definition ONE_ONE {A B : Type'} := fun _2064 : A -> B => forall x1 : A, forall x2 : A, ((_2064 x1) = (_2064 x2)) -> x1 = x2.
+
+Definition ONTO {A B : Type'} := fun _2069 : A -> B => forall y : B, exists x : A, y = (_2069 x).
+
+Lemma axiom_6 : exists f : ind -> ind, (@ONE_ONE ind ind f) /\ (~ (@ONTO ind ind f)).
+Proof.
+  exists S. split. exact eq_add_S. intro h. generalize (h 0). intros [x hx].
+  discriminate.
+Qed.
+
+Definition IND_SUC_pred := fun f : ind -> ind => exists z : ind, (forall x1 : ind, forall x2 : ind, ((f x1) = (f x2)) = (x1 = x2)) /\ (forall x : ind, ~ ((f x) = z)).
+
+Definition IND_SUC := ε IND_SUC_pred.
+
+Lemma IND_SUC_ex : exists f, IND_SUC_pred f.
+Proof.
+  destruct axiom_6 as [f [h1 h2]]. exists f.
+  unfold ONTO in h2. rewrite not_forall_eq in h2. destruct h2 as [z h2]. exists z.
+  split.
+  intros x y. apply prop_ext. apply h1. intro e. rewrite e. reflexivity.
+  rewrite not_exists_eq in h2. intros x e. apply (h2 x). symmetry. exact e.
+Qed.
+
+Lemma IND_SUC_prop : IND_SUC_pred IND_SUC.
+Proof. unfold IND_SUC. apply ε_spec. apply IND_SUC_ex. Qed.
+
+Lemma IND_SUC_inj : ONE_ONE IND_SUC.
+Proof.
+  generalize IND_SUC_prop. intros [z [h1 h2]]. intros x y e. rewrite <- h1.
+  exact e.
+Qed.
+
+Definition IND_0_pred := fun z : ind => (forall x1 : ind, forall x2 : ind, ((IND_SUC x1) = (IND_SUC x2)) = (x1 = x2)) /\ (forall x : ind, ~ ((IND_SUC x) = z)).
+
+Definition IND_0 := ε IND_0_pred.
+
+Lemma IND_0_ex : exists z, IND_0_pred z.
+Proof.
+  generalize IND_SUC_prop. intros [z [h1 h2]]. exists z. split. exact h1. exact h2.
+Qed.
+
+Lemma IND_0_prop : IND_0_pred IND_0.
+Proof. unfold IND_0. apply ε_spec. apply IND_0_ex. Qed.
+
+Lemma IND_SUC_neq_0 i : IND_SUC i <> IND_0.
+Proof. generalize IND_0_prop. intros [h1 h2]. apply h2. Qed.
+
+(****************************************************************************)
+(* Properties of NUM_REP. *)
+(****************************************************************************)
+
+Definition NUM_REP := fun a : ind => forall NUM_REP' : ind -> Prop, (forall a' : ind, ((a' = IND_0) \/ (exists i : ind, (a' = (IND_SUC i)) /\ (NUM_REP' i))) -> NUM_REP' a') -> NUM_REP' a.
+
+Definition NUM_REP' := fun a : ind => forall P : ind -> Prop, (P IND_0 /\ forall i, P i -> P (IND_SUC i)) -> P a.
+
+Lemma NUM_REP_eq : NUM_REP = NUM_REP'.
+Proof.
+  apply fun_ext; intro a. apply prop_ext; intros h P.
+  intros [p0 ps]. apply h. intros a' [i|i].
+    subst a'. exact p0.
+    destruct i as [b [e i]]. subst a'. apply ps. exact i.
+  intro i. apply h. split.
+    apply i. left. reflexivity.
+    intros b pb. apply i. right. exists b. split. reflexivity. exact pb.
+Qed.
+
+Lemma NUM_REP_0 : NUM_REP IND_0.
+Proof. rewrite NUM_REP_eq. intros P [h _]. exact h. Qed.
+
+Lemma NUM_REP_S i : NUM_REP i -> NUM_REP (IND_SUC i).
+Proof.
+  rewrite NUM_REP_eq. intros hi P [h0 hS]. apply hS. apply hi.
+  split. exact h0. exact hS.
+Qed.
+
+Inductive NUM_REP_ID : ind -> Prop :=
+  | NUM_REP_ID_0 : NUM_REP_ID IND_0
+  | NUM_REP_ID_S i : NUM_REP_ID i -> NUM_REP_ID (IND_SUC i).
+
+Lemma NUM_REP_eq_ID : NUM_REP = NUM_REP_ID.
+Proof.
+  apply fun_ext; intro i. apply prop_ext.
+  rewrite NUM_REP_eq. intro h. apply h. split.
+    apply NUM_REP_ID_0.
+    intros j hj. apply NUM_REP_ID_S. exact hj.
+  induction 1. apply NUM_REP_0. apply NUM_REP_S. assumption.
+Qed.
+
+(****************************************************************************)
+(* Alignment of the type of natural numbers. *)
+(****************************************************************************)
+
+Require Import BinNat Lia.
 
 Open Scope N_scope.
 
@@ -15,10 +639,6 @@ Proof.
   intros n1 n2 n12 a1 a2 a12. subst n2. subst a2. reflexivity.
 Qed.
 
-(****************************************************************************)
-(* Alignment of the type of natural numbers. *)
-(****************************************************************************)
-
 Definition dest_num := N.recursion IND_0 (fun _ r => IND_SUC r).
 
 Lemma dest_num0 : dest_num 0 = IND_0.
diff --git a/reproduce b/reproduce
index 4860f32..0998b8c 100755
--- a/reproduce
+++ b/reproduce
@@ -96,7 +96,7 @@ translate_proofs() {
     mkdir -p output
     cd output
     make $jobs clean-all || true
-    hol2dk config $base.ml $root_path ../../logic.v ../../mappings.v BinNat ../../deps.mk ../../erasing.lp
+    hol2dk config $base.ml $root_path ../../mappings.v BinNat ../../deps.mk ../../mappings.lp
     make split
     make $jobs lp
     make $jobs v
diff --git a/terms.v b/terms.v
index 6046894..4c88bd3 100644
--- a/terms.v
+++ b/terms.v
@@ -1,4 +1,4 @@
-Require Import HOLLight_Real_With_N.logic HOLLight_Real_With_N.mappings BinNat.
+Require Import HOLLight_Real_With_N.mappings BinNat.
 Require Import HOLLight_Real_With_N.theory_hol.
 Definition _FALSITY_ : Prop := False.
 Lemma _FALSITY__def : _FALSITY_ = False.
diff --git a/theorems.v b/theorems.v
index f5b7eff..26b6abd 100644
--- a/theorems.v
+++ b/theorems.v
@@ -1,4 +1,4 @@
-Require Import HOLLight_Real_With_N.logic HOLLight_Real_With_N.mappings BinNat.
+Require Import HOLLight_Real_With_N.mappings BinNat.
 Require Import HOLLight_Real_With_N.theory_hol.
 Require Import HOLLight_Real_With_N.terms.
 Axiom thm_T_DEF : True = ((fun p : Prop => p) = (fun p : Prop => p)).
diff --git a/theory_hol.v b/theory_hol.v
index 36f041e..111cf54 100644
--- a/theory_hol.v
+++ b/theory_hol.v
@@ -1,4 +1,4 @@
-Require Import HOLLight_Real_With_N.logic HOLLight_Real_With_N.mappings BinNat.
+Require Import HOLLight_Real_With_N.mappings BinNat.
 Lemma TRANS {a : Type'} {x y z : a} (xy : x = y) (yz : y = z) : x = z.
 Proof. exact (@EQ_MP (x = y) (x = z) (@MK_COMB a Prop (@eq a x) (@eq a x) y z (@eq_refl (a -> Prop) (@eq a x)) yz) xy). Qed.
 Lemma SYM {a : Type'} {x y : a} (xy : x = y) : y = x.