trm true = trm false :> finterval := path_ishprop _ _.
Require Import HoTT.Basics HoTT.Truncations HoTT.Types.Bool. Require Import Metatheory.Core Metatheory.FunextVarieties Metatheory.ImpredicativeTruncation.