Theorem: Float3.x.as_struct_proj (test/deriving/structure_ops.lean)

State before:
⊢ x = fun v => structProj v (Sum.inl ())
Tactic:
rfl
State after:
no goals