proposition: Theorem LH_Gn_0_equiv : forall (n : nat) c, n < numA -> evalDist (LH_Gn n) c == evalDist (LH_G_0 n) c.
proof: Proof. intuition. unfold LH_Gn, LH_G_0. comp_skip; comp_simp. comp_skip. erewrite skipn_S. simpl. inline_first. comp_skip. reflexivity. inline_first. comp_skip. erewrite numA_correct; intuition; eauto. Qed.
imports: FCF CompFold