{l1 l2} : ListEq l1 l2 <~> l1 = l2 := equiv_adjointify decode encode decode_encode encode_decode.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc. Require Import Basics.Equivalences Types.Empty Types.Unit Types.Prod. Require Import Modalities.ReflectiveSubuniverse Truncations.Core. Require Import Spaces.List.Core.