proposition: Lemma cap'_level n m (x y: expr n m): e_level (cap' x y) ≪ CAP+e_level x+e_level y.
proof: Proof. unfold cap'. case is_top_spec. solve_lower'. case is_top_spec. solve_lower'. case is_zer_spec. solve_lower'. case is_zer_spec; solve_lower'. Qed.
imports: kleene syntax powerfix