Skip to content
Snippets Groups Projects
Commit c9a7d94e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Renaming flattening lemma.

parent fa1cf928
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
theories/typing/product.v
+ 1
− 1
View file @ c9a7d94e
...@@ -169,7 +169,7 @@ Section typing. ...@@ -169,7 +169,7 @@ Section typing.
- iExists F, ∅. iFrame. by iPureIntro; set_solver. - iExists F, ∅. iFrame. by iPureIntro; set_solver.
Qed. Qed.
Lemma ty_incl_prod_flatten E L tyl1 tyl2 tyl3 : Lemma subtype_prod_flatten E L tyl1 tyl2 tyl3 :
eqtype E L (Π(tyl1 ++ Π tyl2 :: tyl3)) (Π(tyl1 ++ tyl2 ++ tyl3)). eqtype E L (Π(tyl1 ++ Π tyl2 :: tyl3)) (Π(tyl1 ++ tyl2 ++ tyl3)).
Proof. Proof.
unfold product. induction tyl1; simpl; last by f_equiv. unfold product. induction tyl1; simpl; last by f_equiv.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment