+
+
+(*
+lemma semi_lattice_of_semi_lattice_base: semi_lattice_base → semi_lattice.
+intro slb; apply (mk_semi_lattice (excess_of_semi_lattice_base slb));
+[1: apply (sl_op slb);
+|2: intro x; apply (eq_trans (excess_of_semi_lattice_base slb)); [2:
+ apply (sl_op_refl slb);|1:skip] (sl_op slb x x)); ? (sl_op_refl slb x));
+
+ unfold excess_of_semi_lattice_base; simplify;
+ intro H; elim H;
+ [
+
+
+ lapply (ap_rewl (excess_of_semi_lattice_base slb) x ? (sl_op slb x x)
+ (eq_sym (excess_of_semi_lattice_base slb) ?? (sl_op_refl slb x)) t);
+ change in x with (sl_carr slb);
+ apply (Ap≪ (x ✗ x)); (sl_op_refl slb x));
+
+whd in H; elim H; clear H;
+ [ apply (ap_coreflexive (excess_of_semi_lattice_base slb) (x ✗ x) t);
+
+prelattice (excess_of_directed l_)); [apply (sl_op l_);]
+unfold excess_of_directed; try unfold apart_of_excess; simplify;
+unfold excl; simplify;
+[intro x; intro H; elim H; clear H;
+ [apply (sl_op_refl l_ x);
+ lapply (Ap≫ ? (sl_op_comm ???) t) as H; clear t;
+ lapply (sl_strong_extop l_ ??? H); apply ap_symmetric; assumption
+ | lapply (Ap≪ ? (sl_op_refl ?x) t) as H; clear t;
+ lapply (sl_strong_extop l_ ??? H); apply (sl_op_refl l_ x);
+ apply ap_symmetric; assumption]
+|intros 3 (x y H); cases H (H1 H2); clear H;
+ [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x y)) H1) as H; clear H1;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (sl_op_comm ???) H1); apply (ap_coreflexive ?? Hletin);
+ |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ y x)) H2) as H; clear H2;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (sl_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);]
+|intros 4 (x y z H); cases H (H1 H2); clear H;
+ [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x (sl_op l_ y z))) H1) as H; clear H1;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (eq_sym ??? (sl_op_assoc ?x y z)) H1) as H; clear H1;
+ apply (ap_coreflexive ?? H);
+ |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ (sl_op l_ x y) z)) H2) as H; clear H2;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (Ap≪ ? (sl_op_assoc ?x y z) H1) as H; clear H1;
+ apply (ap_coreflexive ?? H);]
+|intros (x y z H); elim H (H1 H1); clear H;
+ lapply (Ap≪ ? (sl_op_refl ??) H1) as H; clear H1;
+ lapply (sl_strong_extop l_ ??? H) as H1; clear H;
+ lapply (sl_strong_extop l_ ??? H1) as H; clear H1;
+ cases (ap_cotransitive ??? (sl_op l_ y z) H);[left|right|right|left] try assumption;
+ [apply ap_symmetric;apply (Ap≪ ? (sl_op_comm ???));
+ |apply (Ap≫ ? (sl_op_comm ???));
+ |apply ap_symmetric;] assumption;
+|intros 4 (x y H H1); apply H; clear H; elim H1 (H H);
+ lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H;
+ lapply (sl_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric]
+ assumption
+|intros 3 (x y H);
+ cut (sl_op l_ x y ≈ sl_op l_ x (sl_op l_ y y)) as H1;[2:
+ intro; lapply (sl_strong_extop ???? a); apply (sl_op_refl l_ y);
+ apply ap_symmetric; assumption;]
+ lapply (Ap≪ ? (eq_sym ??? H1) H); apply (sl_op_assoc l_ x y y);
+ assumption; ]