simpl. destruct IST_proof as [in1 in2]. destruct in2 as [in2 in3].

- split. apply H. assumption.

apply IHproof. assumption.

simpl. simpl in infSeq. destruct infSeq as [in1 in2].

destruct in2 as [in2 in3].

- apply PcInfSeq_superset.

apply IHproof. assumption.

apply pcInfSeqAxs_subset. assumption.

-Lemma Pc~~InfSeq~~_need_finite_axs: forall T p,

+Lemma PcProof_need_finite_axs: forall T p,

(T |- p) -> exists S, Included _ S T /\ Finite _ S /\ (S |- p).

-induction PrvTp as [proof PrfTp].

-set (S := pcProofAxs proof).

-assert (Included pcProp S T) as Hinc.

-apply pcProofAxs_subset with p. assumption.

+destruct PrvTp as [proof PrfTp].

+ destruct PrfTp as [proof_of_p H].

+ destruct PcInfSeq_need_finite_axs with T (a::proof) as [S Inf].

+ destruct Inf as [incl finite]. destruct finite as [finite infseq].

- apply pcProofAxs_finite with T p. assumption.

+ split. assumption. exists (a::proof). split. assumption.

Theorem PcConsistent_subset: forall T S,