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

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