proposition: Lemma cand_sat : forall X : term -> Prop, is_cand X -> forall T : term, sn T -> forall u : term, sn u -> forall m : term, X (subst u m) -> X (App (Abs T m) u).
proof: Proof. unfold sn in |- *. simple induction 2. simple induction 3. intros. generalize H6. elimtype (sn m); intros. apply (clos_exp X); intros; auto with coc core arith datatypes. red in |- *; intros; discriminate. inversion_clear H10; auto with coc core arith datatypes. inversion_clear H11. apply H2; auto with coc core arith datatypes. apply Acc_intro; auto with coc core arith datatypes. apply H8; auto with coc core arith datatypes. apply (clos_red X) with (subst x0 x1); auto with coc core arith datatypes. unfold subst in |- *; auto with coc core arith datatypes. apply H5; auto with coc core arith datatypes. apply clos_red_star with (subst x0 x1); auto with coc core arith datatypes. unfold subst in |- *; auto with coc core arith datatypes. apply sn_subst with x0. apply (incl_sn X); auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Class