Finite triangular matrices with a dedicated type for the diagonal
elements can be profitably represented by a nested data type, i.e., a
heterogeneous family of inductive data types, while infinite
triangular matrices form an example of a nested coinductive type,
which is a heterogeneous family of coinductive data types. Both kinds
of families are fully supported since the version 8.1 of the Coq
theorem proving environment, released in 2007. Reasoning about nested
coinductive types naturally rests on observational equality, and the
beta release of version 8.2 of Coq greatly helps in using the
rewrite mechanism for Leibniz equality also for the notion of
bisimilarity of infinite triangular matrices. With respect to that
notion of equality, redecoration is shown to form a comonad. The main
result, however, shows how to obtain redecoration through a
redecoration algorithm on infinite streams of finite lists that does
not involve the nested coinductive type. These new results come with a
full formalization in Coq, and limitations of what Coq recognizes as
a guarded definition make the theoretical development more
challenging.