judgemental funext out of HITs

funext.v

Parameter A : Type.
Parameter B : A -> Type.
Parameters f g : forall a : A, B a.
Axiom p : forall x, f x = g x.

Inductive I :=
| zero : I
| one : I
| seg : zero = one.

Definition funext0 (x : I) (a : A) :=
  match x return B a with
    | zero => f a
    | one => g a
    | seg => p a
  end.

Definition funext := funext0 seg.

Check (funext0 seg : f = g).
(* unfold [funext0] *)
Check (((fun (x : I) (a : A) =>
  match x return B a with
    | zero => f a
    | one => g a
    | seg => p a
  end) seg) : f = g).
(* beta reduce *)
Check ((fun a : A =>
  match seg return B a with
    | zero => f a
    | one => g a
    | seg => p a
  end) : f = g).
(* unfold the match *)
Check ((fun a : A => p) : f = g).