take id A ; :: thesis: ( id A is Covariant & id A is feasible )
thus ( id A is Covariant & id A is feasible ) ; :: thesis: verum