Click on a command or tactic to see a detailed view of its use.
%% A single logic approach Kind tm, ty type. Type app tm -> tm -> tm. Type abs ty -> (tm -> tm) -> tm. Type arr ty -> ty -> ty. Type bind tm -> ty -> o. Theorem member_prune : forall L E, nabla (x:tm), member (E x) L -> exists F, E = x\F. Define ctx : olist -> prop by ctx nil ; nabla x, ctx (bind x A :: L) := ctx L. Define of : olist -> tm -> ty -> prop by nabla x, of (L x) x A := nabla x, member (bind x A) (L x) ; of L (app M N) B := exists A, of L M (arr A B) /\ of L N A ; of L (abs A R) (arr A B) := nabla x, of (bind x A :: L) (R x) B. Theorem ctx_uniq : forall L E T1 T2, ctx L -> member (bind E T1) L -> member (bind E T2) L -> T1 = T2.induction on 1. intros. case H1. case H2. case H2. case H3. search. apply member_prune to H5. case H3. apply member_prune to H5. apply IH to H4 H5 H6. search.Theorem type_uniq : forall L E T1 T2, ctx L -> of L E T1 -> of L E T2 -> T1 = T2.