Library Beroal.FunExtEq

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


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

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

Definition ext_eq_dep3 : ∀
        (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),
        (∀ x y z, f0 x y z=f1 x y z) → f0=f1.

Definition forall_args_eq (r : Type)
:= fix rec (args : list Type) : ∀ f0 f1 : FunListArg.type r args, Prop
:= match args
        as args return ∀ f0 f1 : FunListArg.type r args, Prop with
        | nil ⇒ fun f0 f1 ⇒ f0 = f1
        | arg :: argss ⇒ fun f0 f1 ⇒ ∀ 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.