In the linking proofs, [disj_pubfrgnsrc] in [disj_inv] is redundant wrt. [frame_rc] in [rel_inv]. It should probably be removed.
In the linking proofs, [disj_pubfrgnsrc] in [disj_inv] is redundant wrt. [frame_rc] in [rel_inv]. It should probably be removed.