SubjectReduction.agda:24,44-46 .SubjectReduction.♯-1 != (.SubjectReduction.♯-3 eq P Px .s) of type (∞ Stream) when checking that the expression Px has type P (tick (.SubjectReduction.♯-3 eq P Px .s))