Now, the pretty-printer respects the "show implicts" option for propositional equality. Demo: ``` λΠ> (a : Type) -> (n,m,o : Nat) -> (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs (a : Type) -> (n : Nat) -> (m : Nat) -> (o : Nat) -> (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> xs ++ ys ++ zs = (xs ++ ys) ++ zs : Type λΠ> :set showimplicits λΠ> (a : Type) -> (n,m,o : Nat) -> (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect o a) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs (a : Type) -> (n : Prelude.Nat.Nat) -> (m : Prelude.Nat.Nat) -> (o : Prelude.Nat.Nat) -> (xs : Prelude.Vect.Vect n a) -> (ys : Prelude.Vect.Vect m a) -> (zs : Prelude.Vect.Vect o a) -> (=) {A = Prelude.Vect.Vect (Prelude.Nat.plus n (Prelude.Nat.plus m o)) a} {B = Prelude.Vect.Vect (Prelude.Nat.plus (Prelude.Nat.plus n m) o) a} (Prelude.Vect.(++) {m = n} {a = a} {n = Prelude.Nat.plus m o} xs (Prelude.Vect.(++) {m = m} {a = a} {n = o} ys zs)) (Prelude.Vect.(++) {m = Prelude.Nat.plus n m} {a = a} {n = o} (Prelude.Vect.(++) {m = n} {a = a} {n = m} xs ys) zs) : Type ``` This fixes #1410.