proposition: Lemma cap'cap l n m (x y: expr n m) {Hl: CAP+e_level x+e_level y ≪ l}: cap' x y ==_[l] x ∩ y.
proof: Proof. symmetry. unfold cap'. revert Hl. case is_top_spec. intros. apply captx. case is_top_spec. intros. apply capxt. case is_zer_spec. intros. apply capbx. case is_zer_spec. intros. apply capxb. reflexivity. Qed.
imports: kleene syntax powerfix