Library Beroal.FunExtEq

Require Import Coq.Lists.List.
Require Beroal.FunListArg.


Axiom ext_eq_dep : forall
        (ta:Type)
        (tr:ta->Type)
        (f0 f1:forall ta, tr ta),
        (forall a, f0 a=f1 a) -> f0=f1.

Definition ext_eq_dep2 : forall
        (ta0:Type)
        (ta1:ta0->Type)
        (tr:forall a0:ta0, ta1 a0->Type)
        (f0 f1:forall ta0 ta1, tr ta0 ta1),
        (forall x y, f0 x y=f1 x y) -> f0=f1.

Definition ext_eq_dep3 : forall
        (ta0:Type)
        (ta1:ta0->Type)
        (ta2:forall a0:ta0, ta1 a0->Type)
        (tr:forall (a0:ta0) (a1:ta1 a0), ta2 a0 a1->Type)
        (f0 f1:forall ta0 ta1 ta2, tr ta0 ta1 ta2),
        (forall x y z, f0 x y z=f1 x y z) -> f0=f1.

Definition forall_args_eq (r : Type)
:= fix rec (args : list Type) : forall f0 f1 : FunListArg.type r args, Prop
:= match args
        as args return forall f0 f1 : FunListArg.type r args, Prop with
        | nil => fun f0 f1 => f0 = f1
        | arg :: argss => fun f0 f1 => forall x, rec argss (f0 x) (f1 x)
        end.

Definition ext_eq (r : Type) (args : list Type) (f0 f1 : FunListArg.type r args)
        : forall_args_eq r args f0 f1 -> f0=f1.