# Reasoning

[View type-uniq-single.thm]

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.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
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.
induction on 2. intros. case H2.
case H3.
apply ctx_uniq to H1 H4 H5. search.
case H3.
apply IH to H1 H4 H6. search.
case H3.
apply IH to _ H4 H5. search.
```