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