search

vaibhavkarve / igl2020

Lean project for Fall 2020
https://vaibhavkarve.github.io/igl2020/model
7 stars 2 forks source link

add statement and proof of lemma `eq_full_theory_iff_elementary_equivalent` #76

Open vaibhavkarve opened 3 years ago

vaibhavkarve commented 3 years ago

https://github.com/vaibhavkarve/igl2020/blob/7e8efeecc990a28c1c0a3784fb2d44aed5032ad3/src/model.lean#L505

This depends on issue #75. Solve that first.