Theorem: LoVe.BackwardProofs.cong_two_args_1p1 (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
α : Type
a b c d : α
g : α → α → ℕ → α
hab : a = b
hcd : c = d
⊢ g a c (1 + 1) = g b d 2
Tactic:
simp [hab, hcd]
State after:
no goals