proposition: Theorem erase_faithful_leq_clean n m (x y: expr n m): is_clean x -> is_clean y -> l ≪ CKA -> erase x <==_[l] erase y -> x <==_[l] y.
proof: Proof. intros Hx Hy Hl H. assert (H': u_leq (erase x) (erase y)). rewrite <-(syntax_eval_id x), <-(syntax_eval_id y). apply (H u_ops), u_laws. apply eval_erase in Hx. apply eval_erase in Hy. apply H' in Hy as (x'&Hx'&Hxy). now rewrite (eval_fun Hx Hx'). Qed.
imports: kleene syntax