Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : SEV679+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n014.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 06:56:05 PM UTC 2026

% Result   : Theorem 0.74s 0.94s
% Output   : Proof 0.74s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : SEV679+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12  % Command    : run_E %s %d THM
% 0.16/0.34  % Computer : n014.cluster.edu
% 0.16/0.34  % Model    : x86_64 x86_64
% 0.16/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34  % Memory   : 8042.1875MB
% 0.16/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34  % CPULimit   : 300
% 0.16/0.34  % WCLimit    : 300
% 0.16/0.34  % DateTime   : Tue May  5 08:26:53 EDT 2026
% 0.16/0.34  % CPUTime    : 
% 0.74/0.94  % SZS status Theorem
% 0.74/0.94  % SZS output start Proof
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4: ( $i * $i * $i * $i ) > $o)).
% 0.74/0.94  tff(cPLF_2eMaps_2eempty___24a1_type, type, (
% 0.74/0.94     cPLF_2eMaps_2eempty___24a1: $i > $i)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2ety_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2ety: $i)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2: ( $i * $i ) > $o)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2estep___24a2_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2estep___24a2: ( $i * $i ) > $o)).
% 0.74/0.94  tff(cCoq_2eInit_2eDatatypes_2epair___24a4_type, type, (
% 0.74/0.94     cCoq_2eInit_2eDatatypes_2epair___24a4: ( $i * $i * $i * $i ) > $i)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2estore_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2estore: $i)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2etm_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2etm: $i)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2eextends___24a2_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2eextends___24a2: ( $i * $i ) > $o)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2estore__ty___24t_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2estore__ty___24t: $i > $o)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2estore___24t_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2estore___24t: $i > $o)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2ety___24t_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2ety___24t: $i > $o)).
% 0.74/0.94  tff(cPLF_2eReferences_2eSTLCRef_2etm___24t_type, type, (
% 0.74/0.94     cPLF_2eReferences_2eSTLCRef_2etm___24t: $i > $o)).
% 0.74/0.94  tff(1,plain,
% 0.74/0.94      ((~![V0__ST: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))))))) <=> (~![V0__ST: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)) | ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))))),
% 0.74/0.94      inference(rewrite,[status(thm)],[])).
% 0.74/0.94  tff(2,axiom,(~![V0__ST: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''_HAMMER_GOAL'')).
% 0.74/0.94  tff(3,plain,
% 0.74/0.94      (~![V0__ST: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)) | ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))),
% 0.74/0.94      inference(modus_ponens,[status(thm)],[2, 1])).
% 0.74/0.94  tff(4,plain,
% 0.74/0.94      (^[V0__ST: $i] : trans(monotonicity(quant_intro(proof_bind(^[V1__t: $i] : trans(monotonicity(quant_intro(proof_bind(^[V2__t_27: $i] : trans(monotonicity(quant_intro(proof_bind(^[V3__T: $i] : trans(monotonicity(quant_intro(proof_bind(^[V4__st: $i] : trans(monotonicity(quant_intro(proof_bind(^[V5__st_27: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(quant_intro(proof_bind(^[V9__ST_27: $i] : trans(monotonicity(rewrite(((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) <=> (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T))), ((((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) <=> ((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))), rewrite(((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) <=> (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))), ((((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) <=> (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))), (?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) <=> ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))), ((cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))) <=> (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))), rewrite((cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))), ((cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))), ((cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))) <=> (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => ((~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))), rewrite((cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => ((~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))) <=> (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)))), ((cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))) <=> (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st))))), ((cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))) <=> (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)))))), rewrite((cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)))) <=> (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))), ((cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))) <=> (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))), ((cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))) <=> (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))), rewrite((cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))), ((cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))), (![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))) <=> ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))), ((cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))) <=> (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))), rewrite((cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))), ((cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))), (![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))) <=> ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))), ((cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))) <=> (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))), rewrite((cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))), ((cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))), (![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))) <=> ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))), ((cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))))) <=> (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))), rewrite((cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))), ((cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))), (![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))))) <=> ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))), ((cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))))) <=> (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))), rewrite((cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))), ((cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))))), (![V1__t: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))))) <=> ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))), ((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))))))) <=> (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))))), rewrite((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T)))))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)) | ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))), ((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))))))) <=> ((~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)) | ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))))),
% 0.74/0.95      inference(bind,[status(th)],[])).
% 0.74/0.95  tff(5,plain,
% 0.74/0.95      (![V0__ST: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27))))))))))) <=> ![V0__ST: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)) | ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))),
% 0.74/0.95      inference(quant_intro,[status(thm)],[4])).
% 0.74/0.95  tff(6,axiom,(![V0__ST: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST) => ![V1__t: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t) => ![V2__t_27: $i] : (cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27) => ![V3__T: $i] : (cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T) => ![V4__st: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st) => ![V5__st_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27) => (cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T) => (cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st) => (cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27)) => ?[V9__ST_27: $i] : (((cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST)) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T)) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''PLF.References.STLCRef.preservation'')).
% 0.74/0.95  tff(7,plain,
% 0.74/0.95      (![V0__ST: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)) | ![V1__t: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)) | ![V2__t_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)) | ![V3__T: $i] : ((~cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)) | ![V4__st: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)) | ![V5__st_27: $i] : ((~cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)) | ?[V9__ST_27: $i] : (cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27) & cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27, V0__ST) & cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V9__ST_27, V2__t_27, V3__T) & cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27, V5__st_27)) | (~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V1__t, V4__st), cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm, cPLF_2eReferences_2eSTLCRef_2estore, V2__t_27, V5__st_27))) | (~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST, V4__st)) | (~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety), V0__ST, V1__t, V3__T))))))))),
% 0.74/0.95      inference(modus_ponens,[status(thm)],[6, 5])).
% 0.74/0.95  tff(8,plain,
% 0.74/0.95      ($false),
% 0.74/0.95      inference(unit_resolution,[status(thm)],[7, 3])).
% 0.74/0.95  % SZS output end Proof
% 0.87/1.13  % E exiting
%------------------------------------------------------------------------------