proposition: Lemma cforallP N T R : (forall e : env T, R e) -> forall (e : env N), cforall e R.
proof: Proof. move=> Re e; elim: e R Re => [|? e /= IHe e' IHe' ?? x] //=. by apply: IHe => ?; apply: IHe' => /=. Qed.
imports: HB(structures) BinPos BinNat mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq bigop)