Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
4ae4a.. 4a7ef...
Apply unknownprop_67a9b4da3479f0b3ecc9f46f5080b801e2df28e772a8a9215f9b75577fbd1e20 with
4ae4a.. 4a7ef...
The subproof is completed by applying unknownprop_70a9111fbca1264eee8cb9291eadf4d76112dae5d2986289cdc9631de7adb2fc.