case unit
α : Type ?u.16841
β : Type ?u.16844
γ : Type ?u.16847
δ : Type ?u.16850
p : Prop
inst✝ : Decidable p
⊢ _root_.guard p = some PUnit.unit ↔ p
α : Type ?u.16841
β : Type ?u.16844
γ : Type ?u.16847
δ : Type ?u.16850
p : Prop
inst✝ : Decidable p
u : Unit
⊢ _root_.guard p = some u ↔ p
cases u
no goals
case unit
α : Type ?u.16841
β : Type ?u.16844
γ : Type ?u.16847
δ : Type ?u.16850
p : Prop
inst✝ : Decidable p
⊢ _root_.guard p = some PUnit.unit ↔ p
by_cases h : p <;> simp [_root_.guard, h]