Theorem: LoVe.BigStepEquiv.refl (LoVe/Labs/Lab6Solution.lean)

State before:
S : Stmt
s t : State
⊢ (S, s) ⟹ t ↔ (S, s) ⟹ t
Tactic:
rfl
State after:
no goals