proposition: Lemma almost_eq_truncate l : almost_eq (truncate l) l.
proof: Proof. have ? := almost_eq_refl. have ? := almost_eq_false 0 0. have ? := almost_eq_false 0 1. have ? := almost_eq_false 0 2. move: l => [|[] [|[] [|??]]] /=; by do ? constructor. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun