Step
*
of Lemma
system-type_wf
No Annotations
∀[Gamma:j⊢]. ∀[sys:(phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List].
  Gamma, \/(map(λp.(fst(p));sys)) ⊢ system-type(sys) supposing compatible-system{i:l}(Gamma;sys)
BY
{ (Auto THEN InstLemma `system-type-properties` [⌜Gamma⌝;⌜sys⌝]⋅ THEN Auto) }
Latex:
Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[sys:(phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\})  List].
    Gamma,  \mbackslash{}/(map(\mlambda{}p.(fst(p));sys))  \mvdash{}  system-type(sys)  supposing  compatible-system\{i:l\}(Gamma;sys)
By
Latex:
(Auto  THEN  InstLemma  `system-type-properties`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}sys\mkleeneclose{}]\mcdot{}  THEN  Auto)
Home
Index