proposition: Lemma laws_of_injective_morphism {h l X Y} {L: laws h Y} {Hl: l ≪ h} f: @morphism l X Y f -> (forall x y, f x ≦ f y -> x ≦ y) -> (forall x y, f x ≡ f y -> x ≡ y) -> laws l X.
proof: Proof. intros Hf Hleq Hweq. apply (@lower_lattice_laws _ _ _ L) in Hl. clear L. assert (Hleq_iff: forall x y, f x ≦ f y <-> x ≦ y). split. apply Hleq. apply fn_leq. assert (Hweq_iff: forall x y, f x ≡ f y <-> x ≡ y). split. apply Hweq. apply fn_weq. constructor. constructor. intro. apply Hleq. reflexivity. intros x y z. rewrite <-3Hleq_iff. apply Hl. intros. now rewrite <-Hweq_iff, weq_spec, 2Hleq_iff. intros. rewrite <-3Hleq_iff, fn_cup. apply cup_spec. intros. rewrite <-3Hleq_iff, fn_cap. apply cap_spec. right. intros. apply Hleq. rewrite fn_bot. apply leq_bx. right. intros. apply Hleq. rewrite fn_top. apply leq_xt. intros. apply Hleq. rewrite fn_cup, fn_cap, 2fn_cup, fn_cap. apply cupcap_. intros. rewrite <-Hweq_iff. rewrite fn_cap, fn_neg, fn_bot. apply capneg. intros. rewrite <-Hweq_iff. rewrite fn_cup, fn_neg, fn_top. apply cupneg. Qed.
imports: common level