---

Step * of Lemma lift_ctr_wf

[a4,F:Type]. [f:F  a4].  (lift_ctr(f)    F  (  a4))
BY
{ ProveWfLemma }


\mforall{}[a4,F:Type].  \mforall{}[f:F  {}\mrightarrow{}  a4].    (lift\_ctr(f)  \mmember{}  \mBbbZ{}  \mtimes{}  F  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  a4))


By

ProveWfLemma



Home Index