α : Type u
β : Type v
γ : Type w
a : α
f : α → Seq1 β
⊢ join (f a, nil) = f a
α : Type u
β : Type v
γ : Type w
a : α
f : α → Seq1 β
⊢ bind (ret a) f = f a
simp [ret, bind, map]
case mk
α : Type u
β : Type v
γ : Type w
a✝ : α
f : α → Seq1 β
a : β
s : Seq β
⊢ join ((a, s), nil) = (a, s)
α : Type u
β : Type v
γ : Type w
a : α
f : α → Seq1 β
⊢ join (f a, nil) = f a
cases' f a with a s
no goals
case mk
α : Type u
β : Type v
γ : Type w
a✝ : α
f : α → Seq1 β
a : β
s : Seq β
⊢ join ((a, s), nil) = (a, s)
apply recOn s <;> intros <;> simp