proposition: Corollary leq_af : almost_full le.
proof: Proof. unfold almost_full. cut (dec_rel lt). intro decLt. eexists (SUP (af_tree lt_wf decLt)). eapply sec_strengthen. 2: apply secure_from_wf. intros. simpl in H. lia. unfold dec_rel. intros. destruct (le_lt_dec x y). left; lia. right; lia. Defined.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)