Fill auxiliary sorries in Cor 11.10.3 and Prop 11.10.6#497

XPiPiT wants to merge 1 commit intoteorth:mainteorth/analysis:mainfrom

XPiPiT:fix/11-10-3-and-11-10-6-auxiliary-sorriesXPiPiT/analysis:fix/11-10-3-and-11-10-6-auxiliary-sorriesCopy head branch name to clipboard