#elab λ (A : Type) (a : A) (b c : _), if a = b ∧ a = c then tt else ff
