proposition: Lemma Abs_sound : forall (A : term -> Prop) (s : skel) (F : Can s -> term -> Prop) (T m : term), is_can PROP A -> is_can (PROD s PROP) F -> (forall n : term, A n -> forall C : Can s, is_can s C -> eq_can s C C -> F C (subst n m)) -> sn T -> Pi s A F (Abs T m).
proof: Proof. unfold Pi in |- *; simpl in |- *; intros. cut (is_cand (F C)); intros; auto with coc core arith datatypes. apply (clos_exp (F C)); intros; auto with coc core arith datatypes. red in |- *; intros; discriminate. apply clos_red with (App (Abs T m) u); auto with coc core arith datatypes. apply (cand_sat (F C)); auto with coc core arith datatypes. apply (incl_sn A); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class