(P : Type) (a b : P) (p : a = b) : finterval_rec P a b p (trm true) = a := idpath.
Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool. Require Import Metatheory.Core Metatheory.FunextVarieties Metatheory.ImpredicativeTruncation.