proposition: Lemma is_subterm_ok_false : forall s t, is_subterm s t = false -> forall p, subterm_at_pos t p <> Some s.
proof: Proof. intros s t; pattern t; apply term_rec3; clear t. destruct s as [y | ]; simpl; intros x H [ | i p]; simpl. intro Sub; generalize (X.eq_bool_ok x y); rewrite H; intro x_diff_y; apply x_diff_y; injection Sub; exact (fun H => H). discriminate. discriminate. discriminate. destruct s as [x | g k]; intros f l IHl H. intros [ | i p] Sub. discriminate. simpl in H, Sub. revert i Sub; induction l as [ | t l]. intros [ | i] Sub ; discriminate. intros i Sub; case_eq (is_subterm (Var x) t). intro Sub'; rewrite Sub' in H; discriminate. intro nSub; rewrite nSub in H; destruct i as [ | i]; simpl in H. apply (IHl _ (or_introl _ (eq_refl _)) nSub p Sub). simpl in Sub. apply IHl0 with i; trivial. intros; apply IHl; [right | ]; trivial. intros [ | i p]. simpl; intro t_eq_s'; assert (t_eq_s : Term g k = Term f l). injection t_eq_s'; intros; subst; apply eq_refl. clear t_eq_s'; generalize (eq_bool_ok (Term f l) (Term g k)); case_eq (eq_bool (Term f l) (Term g k)); intros H1 H2; simpl in H; simpl in H1; rewrite H1 in H. discriminate. apply H2; rewrite t_eq_s; apply eq_refl. simpl; simpl in H. destruct (if eq_symb_bool f g then (fix eq_bool_list (l1 l2 : list term) : bool := match l1 with | nil => match l2 with | nil => true | _ :: _ => false end | t1 :: k1 => match l2 with | nil => false | t2 :: k2 => if eq_bool t1 t2 then eq_bool_list k1 k2 else false end end) l k else false). discriminate. revert i; simpl in H; induction l as [ | t l]. intros [ | i]; discriminate. intros [ | i]; simpl. apply IHl. left; apply eq_refl. destruct (is_subterm (Term g k) t); [discriminate | apply eq_refl]. apply IHl0. intros; apply IHl; [right | ]; assumption. destruct (is_subterm (Term g k) t); [discriminate | assumption]. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)