Next Types Are Theorems; Programs Are Proofs 32

Final remark

        a -> b :: List a ∧ List b
                ∧ length(a) = length(b)
                ∧ sortedOrder(b)
                ∧ subset(a, b)
                ∧ subset(b, a)

Next Next