lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b).
intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %;
definition hole ≝ λT:Type.λx:T.x.
notation < "\ldots" non associative with precedence 50 for @{'hole}.
definition hole ≝ λT:Type.λx:T.x.
notation < "\ldots" non associative with precedence 50 for @{'hole}.
(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
lemma subst_excess:
(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *)
lemma subst_excess:
notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
notation "'lej'" non associative with precedence 50 for @{'lej}.
notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
notation "'lej'" non associative with precedence 50 for @{'lej}.
-interpretation "Lattice meet" 'meet = (sl_meet (latt_mcarr _)).
-interpretation "Lattice meet_refl" 'meet_refl = (sl_meet_refl (latt_mcarr _)).
-interpretation "Lattice meet_comm" 'meet_comm = (sl_meet_comm (latt_mcarr _)).
-interpretation "Lattice meet_assoc" 'meet_assoc = (sl_meet_assoc (latt_mcarr _)).
-interpretation "Lattice strong_extm" 'strong_extm = (sl_strong_extm (latt_mcarr _)).
-interpretation "Lattice le_to_eqm" 'le_to_eqm = (sl_le_to_eqm (latt_mcarr _)).
-interpretation "Lattice lem" 'lem = (sl_lem (latt_mcarr _)).
-interpretation "Lattice join" 'join = (sl_meet (latt_jcarr _)).
-interpretation "Lattice join_refl" 'join_refl = (sl_meet_refl (latt_jcarr _)).
-interpretation "Lattice join_comm" 'join_comm = (sl_meet_comm (latt_jcarr _)).
-interpretation "Lattice join_assoc" 'join_assoc = (sl_meet_assoc (latt_jcarr _)).
-interpretation "Lattice strong_extm" 'strong_extj = (sl_strong_extm (latt_jcarr _)).
-interpretation "Lattice le_to_eqj" 'le_to_eqj = (sl_le_to_eqm (latt_jcarr _)).
-interpretation "Lattice lej" 'lej = (sl_lem (latt_jcarr _)).
+interpretation "Lattice meet" 'meet = (sl_meet (latt_mcarr ?)).
+interpretation "Lattice meet_refl" 'meet_refl = (sl_meet_refl (latt_mcarr ?)).
+interpretation "Lattice meet_comm" 'meet_comm = (sl_meet_comm (latt_mcarr ?)).
+interpretation "Lattice meet_assoc" 'meet_assoc = (sl_meet_assoc (latt_mcarr ?)).
+interpretation "Lattice strong_extm" 'strong_extm = (sl_strong_extm (latt_mcarr ?)).
+interpretation "Lattice le_to_eqm" 'le_to_eqm = (sl_le_to_eqm (latt_mcarr ?)).
+interpretation "Lattice lem" 'lem = (sl_lem (latt_mcarr ?)).
+interpretation "Lattice join" 'join = (sl_meet (latt_jcarr ?)).
+interpretation "Lattice join_refl" 'join_refl = (sl_meet_refl (latt_jcarr ?)).
+interpretation "Lattice join_comm" 'join_comm = (sl_meet_comm (latt_jcarr ?)).
+interpretation "Lattice join_assoc" 'join_assoc = (sl_meet_assoc (latt_jcarr ?)).
+interpretation "Lattice strong_extm" 'strong_extj = (sl_strong_extm (latt_jcarr ?)).
+interpretation "Lattice le_to_eqj" 'le_to_eqj = (sl_le_to_eqm (latt_jcarr ?)).
+interpretation "Lattice lej" 'lej = (sl_lem (latt_jcarr ?)).
notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
-interpretation "Lattice feq_jl" 'feq_jl = (sl_feq_ml (latt_jcarr _)).
-interpretation "Lattice feq_jr" 'feq_jr = (sl_feq_mr (latt_jcarr _)).
-interpretation "Lattice feq_ml" 'feq_ml = (sl_feq_ml (latt_mcarr _)).
-interpretation "Lattice feq_mr" 'feq_mr = (sl_feq_mr (latt_mcarr _)).
+interpretation "Lattice feq_jl" 'feq_jl = (sl_feq_ml (latt_jcarr ?)).
+interpretation "Lattice feq_jr" 'feq_jr = (sl_feq_mr (latt_jcarr ?)).
+interpretation "Lattice feq_ml" 'feq_ml = (sl_feq_ml (latt_mcarr ?)).
+interpretation "Lattice feq_mr" 'feq_mr = (sl_feq_mr (latt_mcarr ?)).