Agda-2.3.2.2: test/fail/SubjectReduction.err
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))
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))