From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 27 Jul 2018 18:50:11 +0000 (+0200)
Subject: update in basic_2
X-Git-Tag: make_still_working~293
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29;hp=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29;p=helm.git

update in basic_2

+ refinement for native validity (lsubv)
  allows to prove cnv_cpm_trans_lpr_aux (rt-confluence implies validity)
---