proposition: Remark type_Y: forall t, let D := Abs "x" (App (Var "f") (App (Var "x") (Var "x"))) in let Y := Abs "f" (App D D) in nil ⊢ Y ∈ ((t --> t) --> t).
proof: Proof. intros t D Y. Abort. Fixpoint typecheck (E: context) (a: term) : option type := None. Lemma typecheck_sound: forall E a t, typecheck E a = Some t -> has_type E a t. Proof. intros E a; revert a E; induction a; cbn; intros E t T. Abort. Lemma typecheck_complete: forall E a t, has_type E a t -> typecheck E a = Some t. Proof. induction 1; cbn. Abort. Module Subtyping. Inductive type: Type := | Top | Bool | Fun (t1: type) (t2: type). Reserved Notation "t '<:' s" (at level 40). Inductive subtype: type -> type -> Prop := | subtype_top: forall t, t <: Top | subtype_bool: Bool <: Bool | subtype_fun: forall s1 t1 s2 t2, s2 <: s1 -> t1 <: t2 -> Fun s1 t1 <: Fun s2 t2 where "t '<:' s" := (subtype t s). Lemma subtype_refl: forall t, t <: t. Proof. induction t; auto using subtype. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)