proposition: Lemma xforall_spec: forall f s i, xforall f s i = true <-> For_all (fun x => f (i@x) = true) s.
proof: Proof. unfold For_all, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. - now split. - rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. + intros [[Hi Hr] Hl] x. destruct x; simpl; intro H. * apply Hr, H. * apply Hl, H. * rewrite H in Hi. assumption. + intro H; intuition. * specialize (H 1). destruct o. -- apply H. reflexivity. -- reflexivity. * apply H. assumption. * apply H. assumption. Qed.
imports: Bool PeanoNat BinPos OrderedType OrderedTypeEx FSetInterface