partial_fixpoint_aeneas2.lean:104:6-104:15: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:105:6-105:15: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:106:6-106:15: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:107:6-107:15: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:108:6-108:15: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:125:6-125:19: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:126:6-126:23: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:127:6-127:23: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:128:6-128:24: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:129:6-129:31: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:130:6-130:35: warning: declaration uses `sorry`
partial_fixpoint_aeneas2.lean:133:6-133:31: warning: declaration uses `sorry`