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