Commit 4a8ab344 authored by Gaspard Ferey's avatar Gaspard Ferey

Kind not typable.

parent 301fa1ca
......@@ -6,11 +6,11 @@ Require Import conversion.
Inductive Sort : Set := SKind | SType | SObject.
Theorem kind_not_typable2 : forall Γ T t, Γ t : T -> ~ (t = kind).
Proof. intros. induction H; try easy. Qed.
Theorem kind_not_typable : forall Γ T, Γ kind : T -> False.
Proof.
intros.
induction H.
Admitted.
Proof. intros. pose proof (kind_not_typable2 _ _ _ H). easy. Qed.
Lemma not_var_kind_gamma : forall Γ x, Γ -> x : kind Γ -> False.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment