(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.
Require Import Basics.Overture Basics.PathGroupoids. Require Import Types.Paths.