Library typesdecission

Definition makevar_tactic (U:Type) (A:U):=
 exist (fun x:U=>x=A) A (refl_equal A).
Ltac makevar x:=let U:=type of x in
 destruct(makevar_tactic U x).

Tactic Notation "makevar" constr(x):=let U:=type of x in
 destruct(makevar_tactic U x).

Tactic Notation "makevar" constr(x) "as" ident(y) ident(H):=
let U:=type of x in
 destruct(makevar_tactic U x) as [y H].

Lemma eq_leibnitz: forall (A:Type) (x y:A),
(forall (P:A->Prop), P x<->P y) -> x=y.


Lemma inhabited_exists: forall (U:Type),
inhabited U -> exists x:U, True.

Lemma exists_inhabited: forall (U:Type),
(exists x:U, True) -> inhabited U.

Lemma notinhabited_notexists: forall (U:Type),
(~inhabited U )-> (~exists x:U, True).

Lemma notinhabited_rect: forall (U:Type),
(~inhabited U) ->
(forall P:Type,U->P).

Theorem inhabited_types: forall (U:Type),
(inhabited U) -> U<>False.

Theorem inhabited_func: forall (A B:Type),
(inhabited (A->B)) -> inhabited A -> inhabited B.

Theorem empty_func_l: forall (A B:Type),
(~inhabited A) -> inhabited (A->B).

Lemma inhabited_func_trans: forall (A B C:Type),
inhabited (A->B) -> inhabited (B->C) -> inhabited (A->C).

Require Import Classical.
Require Import ClassicalChoice.
Require Import ClassicalEpsilon.
Definition func_break_aux: forall (U:Type),
{R:option (Type*Type)|
(R=None /\ ~exists A:Type, exists B:Type, U=(A->B))\/
(exists A:Type, exists B:Type, U=(A->B) /\ R=Some(A,B)) }.

Definition func_break: forall (U:Type), option (Type*Type).
Defined.

Lemma func_break_base: forall (U:Type),
((func_break U)=None
/\ ~exists A:Type, exists B:Type, U=(A->B))\/
(exists A:Type, exists B:Type, U=(A->B) /\
(func_break U)=Some(A,B)).

Lemma func_break_intro: forall (A B:Type),
(func_break (A->B))=Some (A,B).
Definition func_append_left: forall (A B:Type) (P:B->Prop),
(A->B)->Prop.

Lemma qqq: forall (A B:Type) (P:Type->Prop),
{Q:Type->Prop|Q (A->B) <-> P B}.
Lemma func_equal_r: forall (A B C:Type),
(A->B)=(A->C) -> B=C.