- ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p)
-(* | ProofSymBlock (ens, p) -> *)
-(* let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *)
-(* ProofSymBlock (ens', fix_proof p) *)
+ ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)