proposition: Lemma fn1_unfold l : fn1 l = match l with nil => true | x :: xs => 0 <? length xs + fn0 (length xs) end.
proof: Proof. unfold fn1; simp double_fn. destruct l; now simp double_fn. Qed.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia) List Wellfounded