+lemma subst_excess_preserves_aprtness:
+ ∀l:semi_lattice.
+ ∀e:excess.
+ ∀p,H1,H2.
+ exc_ap l = exc_ap (subst_excess l e p H1 H2).
+intros;
+unfold subst_excess;
+simplify; assumption;
+qed.
+
+
+lemma subst_excess__preserves_aprtness:
+ ∀l:excess.
+ ∀e:excess_base.
+ ∀p,H1,H2.
+ exc_ap l = apartness_OF_excess (subst_excess_ l (subst_dual_excess l (subst_excess_base l e) p) H1 H2).
+intros 3; (unfold subst_excess_; unfold subst_dual_excess; unfold subst_excess_base; unfold exc_ap; unfold mk_excess_dual_smart; simplify);
+(unfold subst_excess_base in p; unfold mk_excess_dual_smart in p; simplify in p);
+intros; cases p;
+reflexivity;
+qed.
+
+lemma subst_excess_base_in_excess_:
+ ∀d:excess_.
+ ∀eb:excess_base.
+ ∀p:exc_carr d = exc_carr eb.
+ excess_.
+intros (e_ eb);
+apply (subst_dual_excess e_);
+ [apply (subst_excess_base e_ eb);
+ |assumption]
+qed.
+
+definition hole ≝ λT:Type.λx:T.x.
+
+notation < "\ldots" non associative with precedence 50 for @{'hole}.
+interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _).
+
+lemma subst_excess_base_in_excess:
+ ∀d:excess.
+ ∀eb:excess_base.
+ ∀p:exc_carr d = exc_carr eb.
+ (∀y1,x1:eb. (?(ap_apart d)) y1 x1 → y1 ≰ x1 ∨ x1 ≰ y1) →
+ (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 → (?(ap_apart d)) y2 x2) →
+ excess.
+[1,3,4:apply Type|2,5:intro f; cases p; apply f]
+intros (d eb p H1 H2);
+apply (subst_excess_ d);
+ [apply (subst_excess_base_in_excess_ d eb p);
+ |apply hole; clear H2;
+ change in ⊢ (%→%→?) with (exc_carr eb);
+ change in ⊢ (?→?→?→? (? % ? ?) (? % ? ?)) with eb; intros (y x H3);
+ apply H1; generalize in match H3;
+ unfold ap_apart; unfold subst_excess_base_in_excess_;
+ unfold subst_dual_excess; simplify;
+ generalize in match x;
+ generalize in match y;
+ cases p; simplify; intros; assumption;
+ |apply hole; clear H1;
+ change in ⊢ (%→%→?) with (exc_carr eb);
+ change in ⊢ (?→?→? (? % ? ?) (? % ? ?)→?) with eb; intros (y x H3);
+ unfold ap_apart; unfold subst_excess_base_in_excess_;
+ unfold subst_dual_excess; simplify; generalize in match (H2 ?? H3);
+ generalize in match x; generalize in match y; cases p;
+ intros; assumption;]
+qed.
+
+lemma tech1: ∀e:excess.
+ ∀eb:excess_base.
+ ∀p,H1,H2.
+ exc_ap e = exc_ap_ (subst_excess_base_in_excess e eb p H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; simplify;
+unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; simplify; reflexivity;
+qed.
+
+lemma tech2:
+ ∀e:excess_.∀eb.∀p.
+ exc_ap e = exc_ap (mk_excess_ (subst_excess_base e eb) (exc_ap e) p).
+intros (e eb p);unfold exc_ap; simplify; cases p; simplify; reflexivity;
+qed.
+
+(*
+lemma eq_fap:
+ ∀a1,b1,a2,b2,a3,b3,a4,b4,a5,b5.
+ a1=b1 → a2=b2 → a3=b3 → a4=b4 → a5=b5 → mk_apartness a1 a2 a3 a4 a5 = mk_apartness b1 b2 b3 b4 b5.
+intros; cases H; cases H1; cases H2; cases H3; cases H4; reflexivity;
+qed.
+*)
+
+lemma subst_excess_base_in_excess_preserves_apartness:
+ ∀e:excess.
+ ∀eb:excess_base.
+ ∀H,H1,H2.
+ apartness_OF_excess e =
+ apartness_OF_excess (subst_excess_base_in_excess e eb H H1 H2).
+intros (e eb p H1 H2);
+unfold subst_excess_base_in_excess;
+unfold subst_excess_; unfold subst_excess_base_in_excess_;
+unfold subst_dual_excess; unfold apartness_OF_excess;
+simplify in ⊢ (? ? ? (? %));
+rewrite < (tech2 e eb);
+reflexivity;
+qed.
+
+alias symbol "nleq" = "Excess base excess".