([[x.hyp]] rho ds < > de e s mk_trace_env(nil, tr.proj) [[x.concl]] rho ds < > de e s mk_trace_env(nil, tr.proj)) Prop
By:
Analyze
THEN
Using [`daa',da]
(BackThru
Thm*p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s:{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da;de) [[p]] rho ds da de e s a tr Prop)
THEN
Try
(BackThru
Thm*v:Top, rho:Decl. v [[ < > ]] rho)
THEN
Reduce 0
Generated subgoals: