proposition: Corollary erase_faithful_weq l n m (x y: expr n m): e_level x + e_level y ≪ l -> l ≪ BOT+CKA -> erase l x ==_[l] erase l y -> x ==_[l] y.
proof: Proof. intros Hxy Hl. rewrite 2weq_spec. split; apply erase_faithful_leq; intuition solve_lower'. Qed.
imports: kleene syntax