Require Import Utf8.
Require Extraction.





(***************)
(* Plato       *)
(***************)

Hypothesis Animals:Type.
Hypothesis plato: Animals.
Hypothesis IsCat : Animals →  Prop.
Hypothesis LikesFish : Animals →  Prop. 

Theorem PlatoLikesFish :
(∀ (x:Animals), IsCat x → LikesFish x)
   → IsCat plato
   → LikesFish plato.
Proof.
  intros HCat Hplato .
  apply (HCat plato).
  apply Hplato.
Defined.

Print PlatoLikesFish.


Definition myproof:=
  λ (HCat: (∀ (x:Animals), IsCat x → LikesFish x)),
   λ (Hplato:IsCat plato),
    (HCat plato Hplato).

Check myproof.


Definition myproof2 A (a:A) (P1:A→Prop) (P2:A→Prop):=
  λ (t:∀x,P1 x→P2 x),
    λ (u:P1 a),
      t a u.

Check myproof2.
Check (myproof2 Animals plato IsCat LikesFish).



(***************)
(* Extraction  *)
(***************)

Lemma transitivity: forall A B C, (A -> B)  -> (B -> C) -> A -> C.
Proof.
  intros A B C H1 H2 H.
  apply H2. apply H1. apply H.
Qed.


Extraction transitivity.


Require Import Euclid Wf_nat.
Extraction Inline gt_wf_rec lt_wf_rec induction_ltof2.
Check eucl_dev.
Print diveucl.
Recursive Extraction eucl_dev.