proposition: Lemma implication_unsized : (forall (C : Type) (H : Checkable C) (b : bool) (c : C), UnsizedChecker (checker c) -> forall s1 s2 : nat, semProdSize (genChecker (implication b c)) s1 <--> semProdSize (genChecker (implication b c)) s2).
proof: Proof. move => C H b c HC s1 s2. move: HC => [/(_ s1 s2) H0]. rewrite /genChecker in H0 *. rewrite -> !semFmapSize in H0; eauto with typeclass_instances. rewrite !semFmapSize. rewrite /implication. case : b; eauto. apply imset_eq. rewrite !semReturnSize. reflexivity. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype) Show Sets Generators Producer RoseTrees Checker Classes