intros (E a b Lab); cases Lab (LEab Aab);
cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)
qed.
intros (E a b Lab); cases Lab (LEab Aab);
cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)
qed.