axiom daemon : ∀x,y:A O.x = y.
alias num (instance 0) = "natural number".
lemma xx : ∀b:B 2.∀a:A 1.eatA ? b = eatB ? a.
intros; [3,5,7,9: apply AB|1: apply daemon];skip.
axiom daemon : ∀x,y:A O.x = y.
alias num (instance 0) = "natural number".
lemma xx : ∀b:B 2.∀a:A 1.eatA ? b = eatB ? a.
intros; [3,5,7,9: apply AB|1: apply daemon];skip.