fact: Definition eta_sum `(z : A + B) : match z with | inl z' => inl z' | inr z' => inr z' end = z := match z with inl _ => 1 | inr _ => 1 end.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall