Agda-2.3.2.2: test/fail/ExistentialsProjections.err
ExistentialsProjections.agda:12,18-26 Variable fwitness is declared irrelevant, so it cannot be used here when checking that the expression fwitness has type A
ExistentialsProjections.agda:12,18-26 Variable fwitness is declared irrelevant, so it cannot be used here when checking that the expression fwitness has type A