proposition: Lemma is_can_Pi : forall (s : skel) (X : term -> Prop), is_cand X -> forall F : Can (PROD s PROP), is_can (PROD s PROP) F -> is_cand (Pi s X F).
proof: Proof. simpl in |- *; unfold Pi in |- *; intros. apply Build_is_cand; intros. apply subterm_sn with (App t (Ref 0)); auto with coc core arith datatypes. apply (incl_sn (F (default_can s))); auto with coc core arith datatypes. apply H1; auto with coc core arith datatypes. apply (var_in_cand 0 X); auto with coc core arith datatypes. apply (clos_red (F C)) with (App t u0); auto with coc core arith datatypes. apply (clos_exp (F C)); auto with coc core arith datatypes. red in |- *; intros; discriminate. generalize H3. cut (sn u). simple induction 1; intros. generalize H1. inversion_clear H10; intros; auto with coc core arith datatypes. elim H10 with T M; auto with coc core arith datatypes. apply (clos_exp (F C)); intros; auto with coc core arith datatypes. red in |- *; intros; discriminate. apply H8 with N2; auto with coc core arith datatypes. apply (clos_red X) with x; auto with coc core arith datatypes. apply (incl_sn X); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class