proposition: Lemma inv_cc : forall E t T, cc E t T -> (exists i (i1 : i < n) (i2 : i < arity (typ f)), t = Vnth ls i1 /\ T = Vnth (inputs (typ f)) i2) \/ (exists x, t = Var x /\ MapsTo x T E /\ ~In x (fvs ls)) \/ (exists v V u, t = App u v /\ cc E u (V ~~> T) /\ cc E v V) \/ (exists x v A B, t = Lam x v /\ T = A ~~> B /\ ~In x (fvs ls) /\ cc (add x A E) v B) \/ (exists g (us : TypArgs g) i (hi : Acc g i), t = Vnth us (Acc_arity hi) /\ T = Vnth (inputs (typ g)) (Acc_arity hi) /\ cc E (apps (Fun g) us) (Base (output_base (typ g)))) \/ (exists g p (us : Tes p), t = apps (Fun g) us /\ T = output (typ g) p /\ 0+p <= arity (typ g) /\ gt1 E (mk_call f ls) (mk_call g us)).
proof: Proof. intros E t T h. inversion h. left. ex i i1 i2. intuition. right. left. exists x. intuition. do 2 right. left. ex u A t0. intuition. do 3 right. left. ex x v A B. intuition. do 4 right. left. ex g us i hi. intuition. do 5 right. ex g p us. intuition. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)