proposition: Lemma fin_all_spec k (p : fin k -> bool) : reflect (forall f, p f = true) (fin_all k p).
proof: Proof. induction k; simp fin_all. constructor. intros f; depelim f. destruct (p fz) eqn:pfz. simpl. specialize (IHk (fun f => p (fs f))). simpl in IHk. destruct IHk; constructor. intros f; depelim f; auto. intro Hf. apply n. intros f'. apply Hf. simpl. constructor. intros H. specialize (H fz). rewrite pfz in H. discriminate. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect