fact: Definition interval_ind (P : interval -> Type) (a : P zero) (b : P one) (p : seg # a = b) : forall x:interval, P x := fun x => (match x return _ -> P x with | zero => fun _ => a | one => fun _ => b end) p.
imports: Basics.Overture Basics.PathGroupoids Types.Paths