exact pure r
case Pure
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
r : R
⊢ motive (construct (FreeF.Pure r))
no goals