%-------------------------------------------------------------------------------------------
include('QCLAxioms.ax').
%---axiom ID entails associated semantic condition
thf(id_corr,conjecture,(
    (vld@(all@^[P:$i>$o]:(cond@P@P))) <=> (![P:$i>$o,W:$i]:(![Z:$i]:((f@W@P@Z)=>(P@Z)))))).
%-------------------------------------------------------------------------------------------