At:
wp2 rel correctness
A:ioa{i:l}(), r:rel(), rho:Decl, de:sig(), e:{[[de]] rho}, a:(
[[A.da]] rho), tr:trace_env([[A.da]] rho). tc_ioa(A;de) 
ioa_mentions_trace(A) 
trace_consistent_rel(rho;A.da;tr.proj;r) 
single_valued_decls(A.ds) 
(
s,x':[[A]] rho de e.state. tc(r;A.ds; < > ;de) 
closed_rel(r) 
covers_rel(A;r) 
[[A]] rho de e.trans(s,a,x') 
(rel_mng_2(r; rho; A.ds; < > ; de; e; s; x';
; tr) 
[[wp2_rel(A;kind(a);r)]] rho A.ds dec_lookup(A.da;kind(a)) de e s value(a) tr))
By:
Repeat ((Analyze 0) THENA (Complete (Auto THEN (Try (Unfold `decl` 0)))))
THEN
Inst
Thm*
A:ioa{i:l}(), r:rel(), rho:Decl, de:sig(), e:{[[de]] rho}, a:(
[[A.da]] rho), tr:trace_env([[A.da]] rho). tc_ioa(A;de) 
ioa_mentions_trace(A) 
trace_consistent_rel(rho;A.da;tr.proj;r) 
single_valued_decls(A.ds) 
(
s,x':[[A]] rho de e.state. tc(r;A.ds;dec_lookup(A.da;kind(a));de) 
covers_rel(A;r) 
[[A]] rho de e.trans(s,a,x') 
(rel_mng_2(r; rho; A.ds; dec_lookup(A.da;kind(a)); de; e; s; x'; value(a); tr) 
[[wp2_rel(A;kind(a);r)]] rho A.ds dec_lookup(A.da;kind(a)) de e s value(a) tr))
[A;r;rho;de;e;a;tr;s]
THEN
SimpleInstHyp x' -1
THEN
RepeatFor 2 ((Analyze -1) THENA Easy)
THEN
NthHypSq -1
THEN
RepeatFor 2 (Analyze THEN (Try Trivial))
THEN
Easy
Generated subgoals:
None
About: