a b c : ℕ,
a_1 : a = b,
a_2 : p (f a) (f b),
h : p (f a) (f a)
facts: {p (f a) (f a), p (f a) (f b), a = b}
equalities: {{b, a}, {f a, f b}}
⊢ p a b
a c : ℕ,
a_1 h₁ : p (f a) (f a)
facts: {p (f a) (f a)}
⊢ p a a
