(** Axiom of extensional equality of functions with dependent types *)

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

Set Implicit Arguments.

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.
Proof.
refine (fun ta0 ta1 tr f0 f1 eq0 => _).
refine (ext_eq_dep _ _ _ _).
refine (fun x => ext_eq_dep _ (f0 x) (f1 x) (eq0 x)).
Qed.

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.
Proof.
refine (fun ta0 ta1 ta2 tr f0 f1 eq0 => _).
refine (ext_eq_dep _ _ _ _).
refine (fun x => ext_eq_dep _ _ _ _).
refine (fun y => ext_eq_dep _ (f0 x y) (f1 x y) (eq0 x y)).
Qed.

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.
Proof.
refine (fun r => _).
refine (fix rec (args : list Type) := _).
destruct args as [|arg argss].
simpl.
	refine (fun _ _ eq0 => eq0).
simpl.
	refine (fun f0 f1 eq0 => _).
	refine (ext_eq_dep _ _ _ (fun x => (rec _ _ _ (eq0 x)))).
Qed.