Description: Obsolete version of f1dom2g as of 25-Sep-2024. (Contributed by Mario Carneiro, 24-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)