proposition: Lemma typing_c_decidable : forall E e, lc_c e -> uniq E -> decidable (exists T, typing_c E e T).
proof: Proof. intros E e LC Uniq. generalize dependent E. induction LC; intros E Uniq. Case "typing_var_c". destruct (@binds_lookup_dec _ x E) as [[T H] | H]. SCase "variable is in environment". left; eauto. SCase "variable not in environment". right. intros [T J]. inversion J; subst; eauto. Case "typing_abs_c". pick fresh x. assert (Fr' : x `notin` L) by auto. destruct (H0 x Fr' ((x ~ T) ++ E)) as [[S J] | J]; eauto. SCase "body typeable". left. exists (typ_arrow T S). pick fresh z and apply typing_abs_c. apply typing_c_rename with (x := x); eauto. SCase "body not typeable". right. intros [S K]. inversion K; subst. apply J. exists T2. pick fresh z. apply typing_c_rename with (x := z); eauto. Case "typing_app_c". destruct (IHLC1 E) as [[T H] | H]; eauto. SCase "function typeable". destruct (IHLC2 E) as [[S J] | J]; eauto. SSCase "argument typeable". destruct T. SSSCase "function has typ_base". right. intros [S' J']. inversion J'; subst. assert (K : typ_base = typ_arrow T1 S'); eauto using typing_c_unique. inversion K. SSSCase "typ_arrow". destruct (eq_typ_dec T1 S). subst. left; eauto. right. intros [S' J']. inversion J'; subst. assert (T0 = S); eauto using typing_c_unique. assert (typ_arrow T1 T2 = typ_arrow T0 S'); eauto using typing_c_unique. inversion H1; subst; eauto using typing_c_unique. SSCase "argument not typeable". right. intros [S' J']. inversion J'; subst; eauto. SCase "function not typeable". right. intros [S' J']. inversion J'; subst; eauto. Qed.
imports: Metalib.Metatheory String