Theorem: LoVe.proof_irrel (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
a : Prop
h₁ h₂ : a
⊢ h₁ = h₂
Tactic:
rfl
State after:
no goals