proposition: Lemma T_Cond_inv: forall E a ifso ifnot t, E ⊢ Cond a ifso ifnot ∈ t -> exists t', E ⊢ a ∈ Bool /\ E ⊢ ifso ∈ t' /\ E ⊢ ifnot ∈ t' /\ t' <: t.
proof: Proof. intros until t; intros TY; dependent induction TY. - exists t; auto using subtype_refl. - edestruct IHTY as (t' & P & Q & R & S); eauto. exists t'; intuition auto. apply subtype_trans with s; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)