join_comm: ∀x,y:l_carr. join x y ≈ join y x;
meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join x y) z;
meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z;
absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;
join_comm: ∀x,y:l_carr. join x y ≈ join y x;
meet_comm: ∀x,y:l_carr. meet x y ≈ meet y x;
join_assoc: ∀x,y,z:l_carr. join x (join y z) ≈ join (join x y) z;
meet_assoc: ∀x,y,z:l_carr. meet x (meet y z) ≈ meet (meet x y) z;
absorbjm: ∀f,g:l_carr. join f (meet f g) ≈ f;